# HG changeset patch
# User wenzelm
# Date 1141839444 -3600
# Node ID 8c0b056a18edb28717c0aa946af7c2ede0d91260
# Parent  47b05ebe106b3338b0cf5915cb9ea2059e8e3cd3
constdecl: always allow 'where';

diff -r 47b05ebe106b -r 8c0b056a18ed doc-src/IsarRef/pure.tex
--- 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
   ;
diff -r 47b05ebe106b -r 8c0b056a18ed src/Pure/Isar/isar_syn.ML
--- 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);