# HG changeset patch
# User ballarin
# Date 1228818624 -3600
# Node ID b5dad96c755a15e9ca20fe6570bd3dfed405995c
# Parent  54d3a31ca0f600fed81dfe50b9c2401c3df20c3d
When adding locales, delay notes until local theory is built.

diff -r 54d3a31ca0f6 -r b5dad96c755a src/FOL/ex/NewLocaleSetup.thy
--- a/src/FOL/ex/NewLocaleSetup.thy	Mon Dec 08 21:33:50 2008 +0100
+++ b/src/FOL/ex/NewLocaleSetup.thy	Tue Dec 09 11:30:24 2008 +0100
@@ -27,7 +27,9 @@
     (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (([], []), []) -- P.opt_begin
       >> (fn ((name, (expr, elems)), begin) =>
           (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
-            (Expression.add_locale_cmd name name expr elems #-> TheoryTarget.begin)));
+            (Expression.add_locale_cmd name name expr elems #>
+              (fn ((target, notes), ctxt) => TheoryTarget.begin target ctxt |>
+                fold (fn (kind, facts) => LocalTheory.notes kind facts #> snd) notes))));
 
 val _ =
   OuterSyntax.improper_command "print_locales" "print locales of this theory" K.diag
diff -r 54d3a31ca0f6 -r b5dad96c755a src/FOL/ex/NewLocaleTest.thy
--- a/src/FOL/ex/NewLocaleTest.thy	Mon Dec 08 21:33:50 2008 +0100
+++ b/src/FOL/ex/NewLocaleTest.thy	Tue Dec 09 11:30:24 2008 +0100
@@ -113,6 +113,12 @@
 print_locale! use_decl thm use_decl_def
 
 
+text {* Foundational versions of theorems *}
+
+thm logic.assoc
+thm logic.lor_def
+
+
 text {* Defines *}
 
 locale logic_def =
diff -r 54d3a31ca0f6 -r b5dad96c755a src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Mon Dec 08 21:33:50 2008 +0100
+++ b/src/Pure/Isar/expression.ML	Tue Dec 09 11:30:24 2008 +0100
@@ -19,9 +19,11 @@
 
   (* Declaring locales *)
   val add_locale_cmd: string -> bstring -> expression -> Element.context list -> theory ->
-    string * Proof.context
+    (string * (string * (Attrib.binding * (thm list * Attrib.src list) list) list) list) *
+    Proof.context
   val add_locale: string -> bstring -> expression_i -> Element.context_i list -> theory ->
-    string * Proof.context
+    (string * (string * (Attrib.binding * (thm list * Attrib.src list) list) list) list) *
+    Proof.context
 
   (* Interpretation *)
   val sublocale_cmd: string -> expression -> theory -> Proof.state;
@@ -766,14 +768,13 @@
       (body_elems |> map_filter (fn Fixes fixes => SOME fixes | _ => NONE) |> flat);
     val asm = if is_some b_statement then b_statement else a_statement;
     val (body_elems', defns) = fold_map (defines_to_notes thy') body_elems [];
-    val notes = body_elems' |>
-      (fn elems => fold_map assumes_to_notes elems (map Element.conclude_witness a_axioms)) |>
-      fst |> map (Element.morph_ctxt satisfy) |>
-      map_filter (fn Notes notes => SOME notes | _ => NONE) |>
-      (if is_some asm
-        then cons (Thm.internalK, [((Binding.name (bname ^ "_" ^ axiomsN), []),
-          [([assume (cterm_of thy' (the asm))], [(Attrib.internal o K) NewLocale.witness_attrib])])])
-        else I);
+
+    val notes =
+        if is_some asm
+        then [(Thm.internalK, [((Binding.name (bname ^ "_" ^ axiomsN), []),
+          [([Assumption.assume (cterm_of thy' (the asm))],
+            [(Attrib.internal o K) NewLocale.witness_attrib])])])]
+        else [];
 
     val deps' = map (fn (l, morph) => (l, morph $> satisfy)) deps;
 
@@ -781,8 +782,15 @@
       NewLocale.register_locale bname (extraTs, params)
         (asm, defns) ([], [])
         (map (fn n => (n, stamp ())) notes |> rev) (map (fn d => (d, stamp ())) deps' |> rev) |>
-      NewLocale.init name
-  in (name, loc_ctxt) end;
+      NewLocale.init name;
+
+    (* These will be added in the local theory. *)
+    val notes' = body_elems' |>
+      (fn elems => fold_map assumes_to_notes elems (map Element.conclude_witness a_axioms)) |>
+      fst |> map (Element.morph_ctxt satisfy) |>
+      map_filter (fn Notes notes => SOME notes | _ => NONE);
+
+  in ((name, notes'), loc_ctxt) end;
 
 in
 
diff -r 54d3a31ca0f6 -r b5dad96c755a src/Pure/Isar/new_locale.ML
--- a/src/Pure/Isar/new_locale.ML	Mon Dec 08 21:33:50 2008 +0100
+++ b/src/Pure/Isar/new_locale.ML	Tue Dec 09 11:30:24 2008 +0100
@@ -39,7 +39,6 @@
     Proof.context -> Proof.context
   val activate_global_facts: string * Morphism.morphism -> theory -> theory
   val activate_local_facts: string * Morphism.morphism -> Proof.context -> Proof.context
-(*  val activate: string -> theory -> (Element.context_i -> 'a -> 'a) -> 'a -> 'a *)
   val init: string -> theory -> Proof.context
 
   (* Reasoning about locales *)