warning in proper transaction context;
authorwenzelm
Tue Jul 20 21:57:26 2010 +0200 (2010-07-20 ago)
changeset 37861e1f028a8c76a
parent 37860 aa3b3d00698b
child 37862 ec81023c6861
warning in proper transaction context;
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Jul 20 21:49:39 2010 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Jul 20 21:57:26 2010 +0200
     1.3 @@ -184,9 +184,9 @@
     1.4  val _ =
     1.5    Outer_Syntax.command "axioms" "state arbitrary propositions (axiomatic!)" Keyword.thy_decl
     1.6      (Scan.repeat1 Parse_Spec.spec >>
     1.7 -      (Toplevel.theory o
     1.8 -        (Isar_Cmd.add_axioms o
     1.9 -          tap (fn _ => legacy_feature "Old 'axioms' command -- use 'axiomatization' instead"))));
    1.10 +      (fn spec => Toplevel.theory (fn thy =>
    1.11 +        (legacy_feature "Old 'axioms' command -- use 'axiomatization' instead";
    1.12 +          Isar_Cmd.add_axioms spec thy))));
    1.13  
    1.14  val opt_unchecked_overloaded =
    1.15    Scan.optional (Parse.$$$ "(" |-- Parse.!!!