# HG changeset patch
# User wenzelm
# Date 1026837611 -7200
# Node ID 3e270e61133aca36322ea466f8f30f0e173e1e8c
# Parent  33b7736d8cc0462f6629949d93949d18b4049f80
add_locale: adapted args;

diff -r 33b7736d8cc0 -r 3e270e61133a src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Tue Jul 16 18:39:55 2002 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Tue Jul 16 18:40:11 2002 +0200
@@ -146,7 +146,8 @@
   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
@@ -570,8 +571,9 @@
 
 (* 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 *)