src/Pure/Isar/isar_syn.ML
changeset 21601 6588b947d631
parent 21527 7140f8aba380
child 21705 0f3ad56548bc
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Nov 29 23:33:09 2006 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Nov 30 14:17:22 2006 +0100
     1.3 @@ -188,32 +188,43 @@
     1.4        >> (Toplevel.theory o IsarCmd.add_defs));
     1.5  
     1.6  
     1.7 -(* constant definitions and abbreviations *)
     1.8 +(* old constdefs *)
     1.9  
    1.10 -val constdecl =
    1.11 -  (P.name --| P.$$$ "where") >> (fn x => (x, NONE, NoSyn)) ||
    1.12 -    P.name -- (P.$$$ "::" |-- P.!!! P.typ >> SOME) -- P.opt_mixfix'
    1.13 -      --| Scan.option (P.$$$ "where") >> P.triple1 ||
    1.14 -    P.name -- (P.mixfix >> pair NONE) --| Scan.option (P.$$$ "where") >> P.triple2;
    1.15 +val old_constdecl =
    1.16 +  P.name --| P.where_ >> (fn x => (x, NONE, NoSyn)) ||
    1.17 +  P.name -- (P.$$$ "::" |-- P.!!! P.typ >> SOME) -- P.opt_mixfix'
    1.18 +    --| Scan.option P.where_ >> P.triple1 ||
    1.19 +  P.name -- (P.mixfix >> pair NONE) --| Scan.option P.where_ >> P.triple2;
    1.20  
    1.21 -val constdef = Scan.option constdecl -- (P.opt_thm_name ":" -- P.prop);
    1.22 +val old_constdef = Scan.option old_constdecl -- (P.opt_thm_name ":" -- P.prop);
    1.23  
    1.24  val structs =
    1.25    Scan.optional ((P.$$$ "(" -- P.$$$ "structure") |-- P.!!! (P.simple_fixes --| P.$$$ ")")) [];
    1.26  
    1.27  val constdefsP =
    1.28    OuterSyntax.command "constdefs" "old-style constant definition" K.thy_decl
    1.29 -    (structs -- Scan.repeat1 constdef >> (Toplevel.theory o Constdefs.add_constdefs));
    1.30 +    (structs -- Scan.repeat1 old_constdef >> (Toplevel.theory o Constdefs.add_constdefs));
    1.31 +
    1.32 +
    1.33 +(* constant definitions and abbreviations *)
    1.34 +
    1.35 +val constdecl =
    1.36 +  P.name --
    1.37 +    (P.where_ >> K (NONE, NoSyn) ||
    1.38 +      P.$$$ "::" |-- P.!!! ((P.typ >> SOME) -- P.opt_mixfix' --| P.where_) ||
    1.39 +      Scan.ahead (P.$$$ "(") |-- P.!!! (P.mixfix' --| P.where_ >> pair NONE))
    1.40 +  >> P.triple2;
    1.41 +
    1.42 +val constdef = Scan.option constdecl -- (P.opt_thm_name ":" -- P.prop);
    1.43  
    1.44  val definitionP =
    1.45    OuterSyntax.command "definition" "constant definition" K.thy_decl
    1.46 -    (P.opt_locale_target -- Scan.repeat1 constdef
    1.47 +    (P.opt_locale_target -- (constdef >> single)
    1.48      >> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.definition args)));
    1.49  
    1.50  val abbreviationP =
    1.51    OuterSyntax.command "abbreviation" "constant abbreviation" K.thy_decl
    1.52 -    (P.opt_locale_target -- opt_mode --
    1.53 -      Scan.repeat1 (Scan.option constdecl -- P.prop)
    1.54 +    (P.opt_locale_target -- opt_mode -- (Scan.option constdecl -- P.prop >> single)
    1.55      >> (fn ((loc, mode), args) =>
    1.56          Toplevel.local_theory loc (Specification.abbreviation mode args)));
    1.57  
    1.58 @@ -230,7 +241,7 @@
    1.59    OuterSyntax.command "axiomatization" "axiomatic constant specification" K.thy_decl
    1.60      (P.opt_locale_target --
    1.61       (Scan.optional P.fixes [] --
    1.62 -      Scan.optional (P.$$$ "where" |-- P.!!! (P.and_list1 P.spec)) [])
    1.63 +      Scan.optional (P.where_ |-- P.!!! (P.and_list1 P.spec)) [])
    1.64      >> (fn (loc, (x, y)) => Toplevel.local_theory loc (#2 o Specification.axiomatization x y)));
    1.65  
    1.66  
    1.67 @@ -481,7 +492,7 @@
    1.68  val obtainP =
    1.69    OuterSyntax.command "obtain" "generalized existence"
    1.70      (K.tag_proof K.prf_asm_goal)
    1.71 -    (P.parname -- Scan.optional (P.fixes --| P.$$$ "where") [] -- P.statement
    1.72 +    (P.parname -- Scan.optional (P.fixes --| P.where_) [] -- P.statement
    1.73        >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain x y z)));
    1.74  
    1.75  val guessP =