src/Pure/Isar/method.ML
changeset 25699 891fe6b71d3b
parent 25270 2ed7b34f58e6
child 25957 2cfb703fa8d8
     1.1 --- a/src/Pure/Isar/method.ML	Tue Dec 18 19:54:32 2007 +0100
     1.2 +++ b/src/Pure/Isar/method.ML	Tue Dec 18 19:54:33 2007 +0100
     1.3 @@ -351,7 +351,7 @@
     1.4  val tactic_ref = ref ((fn _ => raise Match): Proof.context -> thm list -> tactic);
     1.5  fun set_tactic f = tactic_ref := f;
     1.6  
     1.7 -fun ml_tactic txt ctxt = CRITICAL (fn () =>
     1.8 +fun ml_tactic txt ctxt = NAMED_CRITICAL "ML" (fn () =>
     1.9    (ML_Context.use_mltext
    1.10      ("let fun tactic (ctxt: Proof.context) (facts: thm list) : tactic =\n"
    1.11        ^ txt ^ "\nin Method.set_tactic tactic end") false (SOME (Context.Proof ctxt));