# HG changeset patch
# User wenzelm
# Date 954418935 -7200
# Node ID ec9ba98587a9438070b9507102c3490bf201c756
# Parent  e8ef58d6d6ebcf3448681e1a1c1dfb20c28363fb
'tactic': refer to PureIsar structure;

diff -r e8ef58d6d6eb -r ec9ba98587a9 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Thu Mar 30 14:21:28 2000 +0200
+++ b/src/Pure/Isar/method.ML	Thu Mar 30 14:22:15 2000 +0200
@@ -346,10 +346,10 @@
 
 fun tactic txt ctxt = METHOD (fn facts =>
  (Context.use_mltext
-   ("let fun (tactic: Proof.context -> thm list -> tactic) ctxt facts = \
-    \let val thm = ProofContext.get_thm ctxt and thms = ProofContext.get_thms ctxt in\n"
+   ("let fun (tactic: PureIsar.Proof.context -> thm list -> tactic) ctxt facts = \
+    \let val thm = PureIsar.ProofContext.get_thm ctxt and thms = PureIsar.ProofContext.get_thms ctxt in\n"
     ^ txt ^
-    "\nend in Method.set_tactic tactic end")
+    "\nend in PureIsar.Method.set_tactic tactic end")
   false (Some (ProofContext.theory_of ctxt)); ! tactic_ref ctxt facts));