# HG changeset patch
# User wenzelm
# Date 1279655846 -7200
# Node ID e1f028a8c76a2e877e57658736ca0c4fc0224b01
# Parent  aa3b3d00698b3b51bcc2f08c656d5c93bcbb81f0
warning in proper transaction context;

diff -r aa3b3d00698b -r e1f028a8c76a src/Pure/Isar/isar_syn.ML
--- 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.!!!