# HG changeset patch
# User wenzelm
# Date 1026986968 -7200
# Node ID 9d6363cbaa09b97c476db0c5eb0aea22648dbca9
# Parent  553e7b62680f6351d68271ac139f723081baa954
adapted locale syntax;

diff -r 553e7b62680f -r 9d6363cbaa09 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Jul 18 12:09:08 2002 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Jul 18 12:09:28 2002 +0200
@@ -285,12 +285,11 @@
   Scan.repeat1 P.locale_element >> pair Locale.empty);
 
 val locale_pred =
-  P.$$$ "(" |-- P.!!! ((P.$$$ "open" >> K None || P.name >> Some) --| P.$$$ ")");
+  Scan.optional (P.$$$ "(" |-- P.!!! ((P.$$$ "open" >> K false) --| P.$$$ ")")) true;
 
 val localeP =
   OuterSyntax.command "locale" "define named proof context" K.thy_decl
-    (Scan.option locale_pred -- P.name --
-      (P.$$$ "=" |-- P.!!! locale_val || Scan.succeed (Locale.empty, []))
+    (locale_pred -- P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, [])
       >> (Toplevel.theory o IsarThy.add_locale o (fn ((x, y), (z, w)) => (x, y, z, w))));