--- a/doc-src/IsarRef/pure.tex Wed Mar 08 18:00:00 2006 +0100
+++ b/doc-src/IsarRef/pure.tex Wed Mar 08 18:37:24 2006 +0100
@@ -257,7 +257,7 @@
structs: '(' 'structure' (vars + 'and') ')'
;
- constdecl: (name '::' type) mixfix | (name '::' type) | name 'where' | mixfix
+ constdecl: ((name '::' type) mixfix | (name '::' type)) 'where'? | name 'where'
;
constdef: thmdecl? prop
;
--- a/src/Pure/Isar/isar_syn.ML Wed Mar 08 18:00:00 2006 +0100
+++ b/src/Pure/Isar/isar_syn.ML Wed Mar 08 18:37:24 2006 +0100
@@ -179,8 +179,9 @@
val constdecl =
(P.name --| P.$$$ "where") >> (fn x => (x, NONE, NoSyn)) ||
- P.name -- (P.$$$ "::" |-- P.!!! P.typ >> SOME) -- P.opt_mixfix' >> P.triple1 ||
- P.name -- (P.mixfix >> pair NONE) >> P.triple2;
+ P.name -- (P.$$$ "::" |-- P.!!! P.typ >> SOME) -- P.opt_mixfix'
+ --| Scan.option (P.$$$ "where") >> P.triple1 ||
+ P.name -- (P.mixfix >> pair NONE) --| Scan.option (P.$$$ "where") >> P.triple2;
val constdef = Scan.option constdecl -- (P.opt_thm_name ":" -- P.prop);