src/Pure/Isar/isar_syn.ML
changeset 33287 0f99569d23e1
parent 32805 9b535493ac8d
child 33390 5b499f36dd25
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Oct 28 20:49:09 2009 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Oct 28 22:00:35 2009 +0100
     1.3 @@ -222,22 +222,13 @@
     1.4  
     1.5  (* constant definitions and abbreviations *)
     1.6  
     1.7 -val constdecl =
     1.8 -  P.binding --
     1.9 -    (P.where_ >> K (NONE, NoSyn) ||
    1.10 -      P.$$$ "::" |-- P.!!! ((P.typ >> SOME) -- P.opt_mixfix' --| P.where_) ||
    1.11 -      Scan.ahead (P.$$$ "(") |-- P.!!! (P.mixfix' --| P.where_ >> pair NONE))
    1.12 -  >> P.triple2;
    1.13 -
    1.14 -val constdef = Scan.option constdecl -- (SpecParse.opt_thm_name ":" -- P.prop);
    1.15 -
    1.16  val _ =
    1.17    OuterSyntax.local_theory "definition" "constant definition" K.thy_decl
    1.18 -    (constdef >> (fn args => #2 o Specification.definition_cmd args));
    1.19 +    (SpecParse.constdef >> (fn args => #2 o Specification.definition_cmd args));
    1.20  
    1.21  val _ =
    1.22    OuterSyntax.local_theory "abbreviation" "constant abbreviation" K.thy_decl
    1.23 -    (opt_mode -- (Scan.option constdecl -- P.prop)
    1.24 +    (opt_mode -- (Scan.option SpecParse.constdecl -- P.prop)
    1.25      >> (fn (mode, args) => Specification.abbreviation_cmd mode args));
    1.26  
    1.27  val _ =