# HG changeset patch
# User wenzelm
# Date 1011116631 -3600
# Node ID 8b69dcccaabce339d6985f5d6b3e6d654f7ae5c6
# Parent  072e9d582db044147def9d4a7f2c6e1241c7e216
allow empty locales;

diff -r 072e9d582db0 -r 8b69dcccaabc src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Jan 15 17:54:31 2002 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Tue Jan 15 18:43:51 2002 +0100
@@ -293,7 +293,8 @@
 
 val localeP =
   OuterSyntax.command "locale" "define named proof context" K.thy_decl
-    ((P.name --| P.$$$ "=") -- locale_val >> (Toplevel.theory o IsarThy.add_locale o P.triple2));
+    (P.name -- (P.$$$ "=" |-- P.!!! locale_val || Scan.succeed (Locale.empty, []))
+      >> (Toplevel.theory o IsarThy.add_locale o P.triple2));