--- 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 ^ ")");
--- 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));