# HG changeset patch # User wenzelm # Date 1004990445 -3600 # Node ID 5b5ed7eec3a8fbd38856ce1c1aa583996edc1e7d # Parent a9c44895cc8c0bc547998bcbe0aa27d7fc631a39 locale_element: optional typ; diff -r a9c44895cc8c -r 5b5ed7eec3a8 src/Pure/Isar/outer_parse.ML --- 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 ||