# HG changeset patch
# User wenzelm
# Date 1006469070 -3600
# Node ID 71534648d5d4b91940064fc1e91a4c796834928d
# Parent  fda9192d0344f7accf0f2bd53e29134d6f744a97
import locale expression;

diff -r fda9192d0344 -r 71534648d5d4 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Nov 22 23:15:12 2001 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Thu Nov 22 23:44:30 2001 +0100
@@ -283,8 +283,9 @@
 
 val locale_decl =
   (P.name --| P.$$$ "=") --
-    (Scan.repeat1 (P.xname --| P.$$$ "+") -- Scan.repeat (P.locale_element -- P.marg_comment) ||
-      Scan.repeat1 (P.locale_element -- P.marg_comment) >> pair []) >> P.triple2;
+    (P.locale_expr -- Scan.optional
+      (P.$$$ "+" |-- P.!!! (Scan.repeat1 (P.locale_element -- P.marg_comment))) [] ||
+    Scan.repeat1 (P.locale_element -- P.marg_comment) >> pair Locale.empty) >> P.triple2;
 
 val localeP =
   OuterSyntax.command "locale" "define named proof context" K.thy_decl