src/Pure/Isar/isar_thy.ML

   val typed_print_translation: string -> theory -> theory
   val print_ast_translation: string -> theory -> theory
   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 * Locale.expr * Args.src Locale.element list -> theory -> theory
+  val add_locale: bstring option option * 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
   val theory: string * string list * (string * bool) list
     -> Toplevel.transition -> Toplevel.transition

     ("(" ^ quote name ^ ", " ^ txt ^ ")");
 
 
 (* add_locale *)
 
-fun add_locale (name, import, body) thy =
-  Locale.add_locale name import (map (Locale.attribute (Attrib.local_attribute thy)) body) thy;
+fun add_locale (pname, name, import, body) thy =
+  Locale.add_locale pname name import
+    (map (Locale.attribute (Attrib.local_attribute thy)) body) thy;
 
 
 (* theory init and exit *)
 
 fun gen_begin_theory upd name parents files =