Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Isar/isar_cmd.ML
changeset 53171 a5e54d4d9081
parent 52549 802576856527
child 55828 42ac3cfb89f6 
--- a/src/Pure/Isar/isar_cmd.ML	Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Fri Aug 23 20:35:50 2013 +0200
@@ -265,12 +265,11 @@
   Proof.goal (Toplevel.proof_of (diag_state ctxt))
     handle Toplevel.UNDEF => error "No goal present";
 
-val _ =
-  Context.>> (Context.map_theory
-   (ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "state"))
-      (Scan.succeed "Isar_Cmd.diag_state ML_context") #>
-    ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "goal"))
-      (Scan.succeed "Isar_Cmd.diag_goal ML_context")));
+val _ = Theory.setup
+  (ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "state"))
+    (Scan.succeed "Isar_Cmd.diag_state ML_context") #>
+   ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "goal"))
+    (Scan.succeed "Isar_Cmd.diag_goal ML_context"));
 
 
 (* print theorems *)
isabelle