allow empty locales;

--- 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));