Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
'tactic': refer to PureIsar structure;
authorwenzelm
Thu, 30 Mar 2000 14:22:15 +0200
changeset 8613 ec9ba98587a9
parent 8612 e8ef58d6d6eb
child 8614 30cc975727f1
'tactic': refer to PureIsar structure;
src/Pure/Isar/method.ML file | annotate | diff | comparison | revisions 
--- 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));
isabelle