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.
warning in proper transaction context;
authorwenzelm
Tue, 20 Jul 2010 21:57:26 +0200
changeset 37861 e1f028a8c76a
parent 37860 aa3b3d00698b
child 37862 ec81023c6861
warning in proper transaction context;
src/Pure/Isar/isar_syn.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/isar_syn.ML	Tue Jul 20 21:49:39 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Jul 20 21:57:26 2010 +0200
@@ -184,9 +184,9 @@
 val _ =
   Outer_Syntax.command "axioms" "state arbitrary propositions (axiomatic!)" Keyword.thy_decl
     (Scan.repeat1 Parse_Spec.spec >>
-      (Toplevel.theory o
-        (Isar_Cmd.add_axioms o
-          tap (fn _ => legacy_feature "Old 'axioms' command -- use 'axiomatization' instead"))));
+      (fn spec => Toplevel.theory (fn thy =>
+        (legacy_feature "Old 'axioms' command -- use 'axiomatization' instead";
+          Isar_Cmd.add_axioms spec thy))));
 
 val opt_unchecked_overloaded =
   Scan.optional (Parse.$$$ "(" |-- Parse.!!!
isabelle