# HG changeset patch
# User wenzelm
# Date 1026986984 -7200
# Node ID bd976af8bf18f411c50576a0a692ce4f1c596e04
# Parent  9d6363cbaa09b97c476db0c5eb0aea22648dbca9
adapted add_locale;

diff -r 9d6363cbaa09 -r bd976af8bf18 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Thu Jul 18 12:09:28 2002 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Thu Jul 18 12:09:44 2002 +0200
@@ -146,8 +146,7 @@
   val token_translation: string -> theory -> theory
   val method_setup: bstring * string * string -> theory -> theory
   val add_oracle: bstring * string -> theory -> theory
-  val add_locale: bstring option option * bstring * Locale.expr * Args.src Locale.element list
-    -> theory -> theory
+  val add_locale: bool * bstring * Locale.expr * Args.src Locale.element list -> theory -> theory
   val begin_theory: string -> string list -> (string * bool) list -> theory
   val end_theory: theory -> theory
   val kill_theory: string -> unit
@@ -571,8 +570,8 @@
 
 (* add_locale *)
 
-fun add_locale (pname, name, import, body) thy =
-  Locale.add_locale pname name import
+fun add_locale (do_pred, name, import, body) thy =
+  Locale.add_locale do_pred name import
     (map (Locale.attribute (Attrib.local_attribute thy)) body) thy;