ML tactic: proper context for compile and runtime;

--- a/src/Pure/Isar/method.ML	Sat Jan 20 14:09:18 2007 +0100
+++ b/src/Pure/Isar/method.ML	Sat Jan 20 14:09:19 2007 +0100
@@ -341,14 +341,10 @@
 fun set_tactic f = tactic_ref := f;
 
 fun tactic txt ctxt = METHOD (fn facts =>
-  (ML_Context.use_mltext
-    ("let fun tactic (ctxt: Proof.context) (facts: thm list) : tactic = \
-       \let val thm = ProofContext.get_thm_closure ctxt o PureThy.Name\n\
-       \  and thms = ProofContext.get_thms_closure ctxt o PureThy.Name in\n"
-       ^ txt ^
-       "\nend in Method.set_tactic tactic end")
-    false NONE;
-    ML_Context.setmp (SOME (Context.Proof ctxt)) (! tactic_ref ctxt) facts));
+ (ML_Context.use_mltext
+   ("let fun tactic (ctxt: Proof.context) (facts: thm list) : tactic =\n"
+     ^ txt ^ "\nin Method.set_tactic tactic end") false (SOME (Context.Proof ctxt));
+  ML_Context.setmp (SOME (Context.Proof ctxt)) (! tactic_ref ctxt) facts));