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