1.1 --- a/src/Tools/eqsubst.ML	Fri Mar 13 19:53:09 2009 +0100
     1.2 +++ b/src/Tools/eqsubst.ML	Fri Mar 13 19:58:26 2009 +0100
     1.3 @@ -434,7 +434,7 @@
     1.4  (* inthms are the given arguments in Isar, and treated as eqstep with
     1.5     the first one, then the second etc *)
     1.6  fun eqsubst_meth ctxt occL inthms =
     1.7 -    Method.SIMPLE_METHOD' (eqsubst_tac ctxt occL inthms);
     1.8 +    SIMPLE_METHOD' (eqsubst_tac ctxt occL inthms);
     1.9  
    1.10  (* apply a substitution inside assumption j, keeps asm in the same place *)
    1.11  fun apply_subst_in_asm i th rule ((cfvs, j, ngoalprems, pth),m) =
    1.12 @@ -548,7 +548,7 @@
    1.13  (* inthms are the given arguments in Isar, and treated as eqstep with
    1.14     the first one, then the second etc *)
    1.15  fun eqsubst_asm_meth ctxt occL inthms =
    1.16 -    Method.SIMPLE_METHOD' (eqsubst_asm_tac ctxt occL inthms);
    1.17 +    SIMPLE_METHOD' (eqsubst_asm_tac ctxt occL inthms);
    1.18  
    1.19  (* syntax for options, given "(asm)" will give back true, without
    1.20     gives back false *)