src/Pure/Isar/method.ML
changeset 22134 ab01073210e4
parent 22118 16639b216295
child 22586 d2008c5f8d99
     1.1 --- a/src/Pure/Isar/method.ML	Sat Jan 20 14:09:18 2007 +0100
     1.2 +++ b/src/Pure/Isar/method.ML	Sat Jan 20 14:09:19 2007 +0100
     1.3 @@ -341,14 +341,10 @@
     1.4  fun set_tactic f = tactic_ref := f;
     1.5  
     1.6  fun tactic txt ctxt = METHOD (fn facts =>
     1.7 -  (ML_Context.use_mltext
     1.8 -    ("let fun tactic (ctxt: Proof.context) (facts: thm list) : tactic = \
     1.9 -       \let val thm = ProofContext.get_thm_closure ctxt o PureThy.Name\n\
    1.10 -       \  and thms = ProofContext.get_thms_closure ctxt o PureThy.Name in\n"
    1.11 -       ^ txt ^
    1.12 -       "\nend in Method.set_tactic tactic end")
    1.13 -    false NONE;
    1.14 -    ML_Context.setmp (SOME (Context.Proof ctxt)) (! tactic_ref ctxt) facts));
    1.15 + (ML_Context.use_mltext
    1.16 +   ("let fun tactic (ctxt: Proof.context) (facts: thm list) : tactic =\n"
    1.17 +     ^ txt ^ "\nin Method.set_tactic tactic end") false (SOME (Context.Proof ctxt));
    1.18 +  ML_Context.setmp (SOME (Context.Proof ctxt)) (! tactic_ref ctxt) facts));
    1.19  
    1.20  
    1.21