# HG changeset patch
# User ballarin
# Date 1142605360 -3600
# Node ID 89949d8652c38697e8ea4531645b8ca83e748a4d
# Parent  b411f25fff25dd08691e9e69012c0a267783fe34
add_locale(_i) returns internal locale name.

diff -r b411f25fff25 -r 89949d8652c3 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Mar 17 14:20:24 2006 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Fri Mar 17 15:22:40 2006 +0100
@@ -342,7 +342,7 @@
     ((P.opt_keyword "open" >> not) -- P.name
         -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, [])
       >> (Toplevel.theory_context o (fn ((is_open, name), (expr, elems)) =>
-          Locale.add_locale is_open name expr elems)));
+             Locale.add_locale is_open name expr elems #> (fn (_, ctxt, thy) => (ctxt, thy)))));
 
 val opt_inst =
   Scan.optional (P.$$$ "[" |-- P.!!! (Scan.repeat1 (P.maybe P.term) --| P.$$$ "]")) [];
diff -r b411f25fff25 -r 89949d8652c3 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Fri Mar 17 14:20:24 2006 +0100
+++ b/src/Pure/Isar/locale.ML	Fri Mar 17 15:22:40 2006 +0100
@@ -72,9 +72,9 @@
   val print_local_registrations: bool -> string -> Proof.context -> unit
 
   val add_locale: bool -> bstring -> expr -> Element.context list -> theory
-    -> Proof.context (*body context!*) * theory
+    -> string * Proof.context (*body context!*) * theory
   val add_locale_i: bool -> bstring -> expr -> Element.context_i list -> theory
-    -> Proof.context (*body context!*) * theory
+    -> string * Proof.context (*body context!*) * theory
 
   (* Storing results *)
   val note_thmss: string -> xstring ->
@@ -1708,7 +1708,7 @@
         lparams = map #1 (params_of body_elemss),
         abbrevs = [],
         regs = []};
-  in (ProofContext.transfer thy' body_ctxt, thy') end;
+  in (name, ProofContext.transfer thy' body_ctxt, thy') end;
 
 in
 
@@ -1718,8 +1718,8 @@
 end;
 
 val _ = Context.add_setup
- (add_locale_i true "var" empty [Fixes [(Syntax.internal "x", NONE, NoSyn)]] #> snd #>
-  add_locale_i true "struct" empty [Fixes [(Syntax.internal "S", NONE, Structure)]] #> snd);
+ (add_locale_i true "var" empty [Fixes [(Syntax.internal "x", NONE, NoSyn)]] #> #3 #>
+  add_locale_i true "struct" empty [Fixes [(Syntax.internal "S", NONE, Structure)]] #> #3);
 
 
 
diff -r b411f25fff25 -r 89949d8652c3 src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Fri Mar 17 14:20:24 2006 +0100
+++ b/src/Pure/Tools/class_package.ML	Fri Mar 17 15:22:40 2006 +0100
@@ -316,12 +316,14 @@
 fun add_locale opn name expr body thy =
   thy
   |> Locale.add_locale opn name expr body
+  |> (fn (_, ctxt, thy) => (ctxt, thy))
   ||>> `(fn thy => intro_incr thy name expr)
   |-> (fn (ctxt, intro) => pair ((Sign.full_name thy name, intro), ctxt));
 
 fun add_locale_i opn name expr body thy =
   thy
   |> Locale.add_locale_i opn name expr body
+  |> (fn (_, ctxt, thy) => (ctxt, thy))
   ||>> `(fn thy => intro_incr thy name expr)
   |-> (fn (ctxt, intro) => pair ((name, intro), ctxt));