# HG changeset patch
# User wenzelm
# Date 1005005947 -3600
# Node ID 34c270893ecb4ae2613b25a80ea205bdee96092c
# Parent  4c16bdee47d4663364a99142e276830e27efc49f
group locale_element;

diff -r 4c16bdee47d4 -r 34c270893ecb src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Tue Nov 06 01:18:46 2001 +0100
+++ b/src/Pure/Isar/outer_parse.ML	Tue Nov 06 01:19:07 2001 +0100
@@ -305,15 +305,15 @@
 
 val loc_mixfix = $$$ "(" -- $$$ "structure" -- !!! ($$$ ")") >> K None || opt_mixfix >> Some;
 
-val locale_element =
-  $$$ "fixes" |-- !!! (and_list1 (name -- Scan.option ($$$ "::" |-- typ) -- loc_mixfix >> triple1))
-    >> Locale.Fixes ||
+val locale_element = group "locale element"
+  ($$$ "fixes" |-- !!! (and_list1 (name -- Scan.option ($$$ "::" |-- typ) -- loc_mixfix
+    >> triple1)) >> Locale.Fixes ||
   $$$ "assumes" |-- !!! (and_list1 (opt_thm_name ":" -- Scan.repeat1 propp))
     >> Locale.Assumes ||
   $$$ "defines" |-- !!! (and_list1 (opt_thm_name ":" -- propp'))
     >> Locale.Defines ||
   $$$ "notes" |-- !!! (and_list1 (opt_thm_name "=" -- xthms1)) >> Locale.Notes ||
-  $$$ "uses" |-- (!!! ($$$ "FIXME" >> K ())) >> Locale.Uses;
+  $$$ "uses" |-- (!!! ($$$ "FIXME" >> K ())) >> Locale.Uses);
 
 
 (* proof methods *)