--- a/src/Pure/Isar/outer_parse.ML Mon Nov 05 20:59:35 2001 +0100
+++ b/src/Pure/Isar/outer_parse.ML Mon Nov 05 21:00:45 2001 +0100
@@ -306,7 +306,7 @@
val loc_mixfix = $$$ "(" -- $$$ "structure" -- !!! ($$$ ")") >> K None || opt_mixfix >> Some;
val locale_element =
- $$$ "fixes" |-- !!! (and_list1 (name -- ($$$ "::" |-- typ) -- loc_mixfix >> triple1))
+ $$$ "fixes" |-- !!! (and_list1 (name -- Scan.option ($$$ "::" |-- typ) -- loc_mixfix >> triple1))
>> Locale.Fixes ||
$$$ "assumes" |-- !!! (and_list1 (opt_thm_name ":" -- Scan.repeat1 propp))
>> Locale.Assumes ||