# HG changeset patch
# User wenzelm
# Date 1114278640 -7200
# Node ID 652e53c4a1ed945fa2df8d88ebbf6574c4d89003
# Parent  ad483e324b5910833a79f1070720e94757852971
removed structure PureIsar;

diff -r ad483e324b59 -r 652e53c4a1ed src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Sat Apr 23 19:50:23 2005 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Sat Apr 23 19:50:40 2005 +0200
@@ -595,7 +595,7 @@
     "val thm = PureThy.get_thm_closure (Context.the_context ());\n\
     \val thms = PureThy.get_thms_closure (Context.the_context ());\n\
     \val method: bstring * (Method.src -> Proof.context -> Proof.method) * string"
-    "PureIsar.Method.add_method method"
+    "Method.add_method method"
     ("(" ^ Library.quote name ^ ", " ^ txt ^ ", " ^ Library.quote cmt ^ ")");
 
 
diff -r ad483e324b59 -r 652e53c4a1ed src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Sat Apr 23 19:50:23 2005 +0200
+++ b/src/Pure/Isar/method.ML	Sat Apr 23 19:50:40 2005 +0200
@@ -488,11 +488,11 @@
 
 fun tactic txt ctxt = METHOD (fn facts =>
   (Context.use_mltext
-    ("let fun tactic (ctxt: PureIsar.Proof.context) (facts: thm list) : tactic = \
-     \let val thm = PureIsar.ProofContext.get_thm_closure ctxt o rpair NONE\n\
-     \  and thms = PureIsar.ProofContext.get_thms_closure ctxt o rpair NONE in\n"
+    ("let fun tactic (ctxt: Proof.context) (facts: thm list) : tactic = \
+     \let val thm = ProofContext.get_thm_closure ctxt o rpair NONE\n\
+     \  and thms = ProofContext.get_thms_closure ctxt o rpair NONE in\n"
      ^ txt ^
-     "\nend in PureIsar.Method.set_tactic tactic end")
+     "\nend in Method.set_tactic tactic end")
     false NONE;
     Context.setmp (SOME (ProofContext.theory_of ctxt)) (! tactic_ref ctxt) facts));