src/Pure/Isar/method.ML
changeset 26455 1757a6e049f4
parent 26435 bdce320cd426
child 26463 9283b4185fdf
     1.1 --- a/src/Pure/Isar/method.ML	Thu Mar 27 21:49:10 2008 +0100
     1.2 +++ b/src/Pure/Isar/method.ML	Fri Mar 28 00:02:54 2008 +0100
     1.3 @@ -354,9 +354,9 @@
     1.4  fun set_tactic f = tactic_ref := f;
     1.5  
     1.6  fun ml_tactic (txt, pos) ctxt = NAMED_CRITICAL "ML" (fn () =>
     1.7 -  (ML_Context.use_mltext false pos
     1.8 +  (ML_Context.eval_in (SOME (Context.Proof ctxt)) false pos
     1.9      ("let fun tactic (ctxt: Proof.context) (facts: thm list) : tactic =\n"
    1.10 -      ^ txt ^ "\nin Method.set_tactic tactic end") (SOME (Context.Proof ctxt));
    1.11 +      ^ txt ^ "\nin Method.set_tactic tactic end");
    1.12      Context.setmp_thread_data (SOME (Context.Proof ctxt)) (! tactic_ref ctxt)));
    1.13  
    1.14  fun tactic txt ctxt = METHOD (ml_tactic txt ctxt);
    1.15 @@ -447,7 +447,7 @@
    1.16  (* method_setup *)
    1.17  
    1.18  fun method_setup name (txt, pos) cmt =
    1.19 -  ML_Context.use_let pos
    1.20 +  ML_Context.expression pos
    1.21      "val method: bstring * (Method.src -> Proof.context -> Proof.method) * string"
    1.22      "Context.map_theory (Method.add_method method)"
    1.23      ("(" ^ quote name ^ ", " ^ txt ^ ", " ^ quote cmt ^ ")")