--- 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);