01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: //
10:
11: /* Generated by Together */
12:
13: package de.uka.ilkd.key.logic.op;
14:
15: import de.uka.ilkd.key.logic.Name;
16: import de.uka.ilkd.key.logic.Term;
17: import de.uka.ilkd.key.logic.WaryClashFreeSubst;
18:
19: public class WarySubstOp extends SubstOp {
20:
21: WarySubstOp(Name name) {
22: super (name);
23: }
24:
25: /**
26: * Apply this substitution operator to <code>term</code>, which
27: * has this operator as top-level operator
28: */
29: public Term apply(Term term) {
30: QuantifiableVariable v = term.varsBoundHere(1)
31: .getQuantifiableVariable(0);
32: WaryClashFreeSubst cfSubst = new WaryClashFreeSubst(v, term
33: .sub(0));
34: Term res = cfSubst.apply(term.sub(1));
35: return res;
36: }
37: }
|