# HG changeset patch
# User wenzelm
# Date 1169298559 -3600
# Node ID ab01073210e443579b0be8c4f3fb1d21e0f62c70
# Parent  dd8a81e84a1c78f876ef246dc78e643b913c1a67
ML tactic: proper context for compile and runtime;

diff -r dd8a81e84a1c -r ab01073210e4 src/Pure/Isar/method.ML
--- 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));