--- 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 *)