diff -r 6f43714517ee -r 08c8dad8e399 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Feb 11 18:51:00 2005 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sun Feb 13 17:15:14 2005 +0100
@@ -186,9 +186,9 @@
   Scan.optional ((P.$$$ "(" -- P.$$$ "structure") |-- P.!!! (vars --| P.$$$ ")")) [];
 
 val constdecl =
-  (P.name --| P.$$$ "where") >> (fn x => (x, None, Syntax.NoSyn)) ||
-    P.name -- (P.$$$ "::" |-- P.!!! P.typ >> Some) -- P.opt_mixfix' >> P.triple1 ||
-    P.name -- (P.mixfix' >> pair None) >> P.triple2;
+  (P.name --| P.$$$ "where") >> (fn x => (x, NONE, Syntax.NoSyn)) ||
+    P.name -- (P.$$$ "::" |-- P.!!! P.typ >> SOME) -- P.opt_mixfix' >> P.triple1 ||
+    P.name -- (P.mixfix' >> pair NONE) >> P.triple2;
 
 val constdef = Scan.option constdecl -- (P.opt_thm_name ":" -- P.prop);