# HG changeset patch
# User haftmann
# Date 1124954703 -7200
# Node ID 76a5a2cc3171e2e16280eb35c751b45a0c3cb69e
# Parent  4b0dc89de43bd69b6890d6fa9d99c3c28e7ca42e
add_locale_context(_i) now exporting elements (still some refinements to be done)

diff -r 4b0dc89de43b -r 76a5a2cc3171 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Aug 25 09:23:40 2005 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Aug 25 09:25:03 2005 +0200
@@ -314,7 +314,7 @@
   OuterSyntax.command "locale" "define named proof context" K.thy_decl
     ((P.opt_keyword "open" >> not) -- P.name
         -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, [])
-      >> (Toplevel.theory_context o (fn ((x, y), (z, w)) => Locale.add_locale_context x y z w)));
+      >> (Toplevel.theory_context o (fn ((x, y), (z, w)) => Locale.add_locale_context x y z w #> (fn ((_, ctxt), thy) => (thy, ctxt)))));
 
 val opt_inst =
   Scan.optional (P.$$$ "[" |-- Scan.repeat1 (P.maybe P.term) --| P.$$$ "]") [];
diff -r 4b0dc89de43b -r 76a5a2cc3171 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Aug 25 09:23:40 2005 +0200
+++ b/src/Pure/Isar/locale.ML	Thu Aug 25 09:25:03 2005 +0200
@@ -74,9 +74,9 @@
 
   (* Storing results *)
   val add_locale_context: bool -> bstring -> expr -> element list -> theory
-    -> theory * ProofContext.context
+    -> (element_i list * ProofContext.context) * theory
   val add_locale_context_i: bool -> bstring -> expr -> element_i list -> theory
-    -> theory * ProofContext.context
+    -> (element_i list * ProofContext.context) * theory
   val add_locale: bool -> bstring -> expr -> element list -> theory -> theory
   val add_locale_i: bool -> bstring -> expr -> element_i list -> theory -> theory
   val smart_note_thmss: string -> string option ->
@@ -2002,24 +2002,25 @@
       (pred_ctxt, axiomify predicate_axioms elemss');
     val export = ProofContext.export_standard predicate_statement ctxt pred_ctxt;
     val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])]));
+    val elems' = List.concat (map #2 (List.filter (equal "" o #1 o #1) elemss'))
   in
     pred_thy
     |> note_thmss_qualified "" name facts' |> #1
     |> declare_locale name
     |> put_locale name {predicate = predicate, import = import,
-        elems = map (fn e => (e, stamp ())) (List.concat (map #2 (List.filter (equal "" o #1 o #1) elemss'))),
+        elems = map (fn e => (e, stamp ())) elems',
         params = (params_of elemss' |>
           map (fn (x, SOME T) => ((x, T), valOf (Symtab.lookup (syn, x)))), map #1 (params_of body_elemss)),
         regs = []}
-    |> rpair body_ctxt
+    |> pair (elems', body_ctxt)
   end;
 
 in
 
 val add_locale_context = gen_add_locale read_context intern_expr;
 val add_locale_context_i = gen_add_locale cert_context (K I);
-fun add_locale b = #1 oooo add_locale_context b;
-fun add_locale_i b = #1 oooo add_locale_context_i b;
+fun add_locale b = #2 oooo add_locale_context b;
+fun add_locale_i b = #2 oooo add_locale_context_i b;
 
 end;