src/Pure/Isar/isar_syn.ML
changeset 35852 4e3fe0b8687b
parent 35835 51c6ac100bd9
child 36112 7fa17a225852
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Sun Mar 21 19:04:46 2010 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun Mar 21 19:28:25 2010 +0100
     1.3 @@ -178,11 +178,9 @@
     1.4  
     1.5  (* axioms and definitions *)
     1.6  
     1.7 -val named_spec = SpecParse.thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y));
     1.8 -
     1.9  val _ =
    1.10    OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl
    1.11 -    (Scan.repeat1 named_spec >> (Toplevel.theory o IsarCmd.add_axioms));
    1.12 +    (Scan.repeat1 SpecParse.spec >> (Toplevel.theory o IsarCmd.add_axioms));
    1.13  
    1.14  val opt_unchecked_overloaded =
    1.15    Scan.optional (P.$$$ "(" |-- P.!!!
    1.16 @@ -191,7 +189,8 @@
    1.17  
    1.18  val _ =
    1.19    OuterSyntax.command "defs" "define constants" K.thy_decl
    1.20 -    (opt_unchecked_overloaded -- Scan.repeat1 named_spec
    1.21 +    (opt_unchecked_overloaded --
    1.22 +      Scan.repeat1 (SpecParse.thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y)))
    1.23        >> (Toplevel.theory o IsarCmd.add_defs));
    1.24  
    1.25