src/Tools/eqsubst.ML
changeset 30510 4120fc59dd85
parent 30318 3d03190d2864
child 30513 1796b8ea88aa
--- a/src/Tools/eqsubst.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/Tools/eqsubst.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -434,7 +434,7 @@
 (* inthms are the given arguments in Isar, and treated as eqstep with
    the first one, then the second etc *)
 fun eqsubst_meth ctxt occL inthms =
-    Method.SIMPLE_METHOD' (eqsubst_tac ctxt occL inthms);
+    SIMPLE_METHOD' (eqsubst_tac ctxt occL inthms);
 
 (* apply a substitution inside assumption j, keeps asm in the same place *)
 fun apply_subst_in_asm i th rule ((cfvs, j, ngoalprems, pth),m) =
@@ -548,7 +548,7 @@
 (* inthms are the given arguments in Isar, and treated as eqstep with
    the first one, then the second etc *)
 fun eqsubst_asm_meth ctxt occL inthms =
-    Method.SIMPLE_METHOD' (eqsubst_asm_tac ctxt occL inthms);
+    SIMPLE_METHOD' (eqsubst_asm_tac ctxt occL inthms);
 
 (* syntax for options, given "(asm)" will give back true, without
    gives back false *)