# HG changeset patch
# User wenzelm
# Date 1333305393 -7200
# Node ID 6523a21076a8071363e1d527fcc7f082574a08cd
# Parent  c0481c3c2a6cffa71036032887a09957a561d6a4
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
more uniform Generic_Target.theory_notes/locale_notes: apply facts to all target contexts;

diff -r c0481c3c2a6c -r 6523a21076a8 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Sun Apr 01 19:07:32 2012 +0200
+++ b/src/Pure/Isar/class.ML	Sun Apr 01 20:36:33 2012 +0200
@@ -552,8 +552,7 @@
     |> synchronize_inst_syntax
     |> Local_Theory.init naming
        {define = Generic_Target.define foundation,
-        notes = Generic_Target.notes
-          (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
+        notes = Generic_Target.notes Generic_Target.theory_notes,
         abbrev = Generic_Target.abbrev
           (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
             Generic_Target.theory_abbrev prmode ((b, mx), t)),
diff -r c0481c3c2a6c -r 6523a21076a8 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Sun Apr 01 19:07:32 2012 +0200
+++ b/src/Pure/Isar/generic_target.ML	Sun Apr 01 20:36:33 2012 +0200
@@ -11,22 +11,26 @@
       term list * term list -> local_theory -> (term * thm) * local_theory) ->
     bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory
-  val notes: (string -> (Attrib.binding * (thm list * Args.src list) list) list ->
+  val notes:
+    (string -> (Attrib.binding * (thm list * Args.src list) list) list ->
       (Attrib.binding * (thm list * Args.src list) list) list -> local_theory -> local_theory) ->
     string -> (Attrib.binding * (thm list * Args.src list) list) list -> local_theory ->
     (string * thm list) list * local_theory
+  val locale_notes: string -> string ->
+    (Attrib.binding * (thm list * Args.src list) list) list ->
+    (Attrib.binding * (thm list * Args.src list) list) list ->
+    local_theory -> local_theory
   val abbrev: (string * bool -> binding * mixfix -> term * term ->
       term list -> local_theory -> local_theory) ->
-    string * bool -> (binding * mixfix) * term -> local_theory ->
-    (term * term) * local_theory
-
+    string * bool -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory
   val background_declaration: declaration -> local_theory -> local_theory
   val standard_declaration: declaration -> local_theory -> local_theory
   val locale_declaration: string -> bool -> declaration -> local_theory -> local_theory
-
   val theory_foundation: ((binding * typ) * mixfix) * (binding * term) ->
     term list * term list -> local_theory -> (term * thm) * local_theory
-  val theory_notes: string -> (Attrib.binding * (thm list * Args.src list) list) list ->
+  val theory_notes: string ->
+    (Attrib.binding * (thm list * Args.src list) list) list ->
+    (Attrib.binding * (thm list * Args.src list) list) list ->
     local_theory -> local_theory
   val theory_abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory -> local_theory
 end
@@ -96,6 +100,8 @@
 
 (* notes *)
 
+local
+
 fun import_export_proof ctxt (name, raw_th) =
   let
     val thy = Proof_Context.theory_of ctxt;
@@ -140,6 +146,11 @@
 
   in (result'', result) end;
 
+fun standard_facts lthy ctxt =
+  Element.transform_facts (Local_Theory.standard_morphism lthy ctxt);
+
+in
+
 fun notes target_notes kind facts lthy =
   let
     val facts' = facts
@@ -150,10 +161,23 @@
     val global_facts = Global_Theory.map_facts #2 facts';
   in
     lthy
-    |> target_notes kind global_facts local_facts
+    |> target_notes kind global_facts (Attrib.partial_evaluation lthy local_facts)
     |> Attrib.local_notes kind local_facts
   end;
 
+fun locale_notes locale kind global_facts local_facts =
+  Local_Theory.background_theory
+    (Attrib.global_notes kind (Attrib.map_facts (K []) global_facts) #> snd) #>
+  (fn lthy => lthy |>
+    Local_Theory.target (fn ctxt => ctxt |>
+      Locale.add_thmss locale kind (standard_facts lthy ctxt local_facts))) #>
+  (fn lthy => lthy |>
+    Local_Theory.map_contexts (fn level => fn ctxt =>
+      if level = 0 orelse level = Local_Theory.level lthy then ctxt
+      else ctxt |> Attrib.local_notes kind (standard_facts lthy ctxt local_facts) |> snd));
+
+end;
+
 
 (* abbrev *)
 
@@ -214,9 +238,13 @@
           (Thm.def_binding_optional b b_def, Logic.mk_equals (lhs, rhs)));
   in ((lhs, def), lthy3) end;
 
-fun theory_notes kind global_facts =
+fun theory_notes kind global_facts local_facts =
   Local_Theory.background_theory (Attrib.global_notes kind global_facts #> snd) #>
-  Local_Theory.target (Attrib.local_notes kind global_facts #> snd);
+  (fn lthy => lthy |> Local_Theory.map_contexts (fn level => fn ctxt =>
+    if level = Local_Theory.level lthy then ctxt
+    else
+      ctxt |> Attrib.local_notes kind
+        (Element.transform_facts (Local_Theory.standard_morphism lthy ctxt) local_facts) |> snd));
 
 fun theory_abbrev prmode ((b, mx), t) =
   Local_Theory.background_theory
diff -r c0481c3c2a6c -r 6523a21076a8 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Sun Apr 01 19:07:32 2012 +0200
+++ b/src/Pure/Isar/named_target.ML	Sun Apr 01 20:36:33 2012 +0200
@@ -101,21 +101,9 @@
 
 (* notes *)
 
-fun locale_notes locale kind global_facts local_facts lthy =
-  let
-    val global_facts' = Attrib.map_facts (K []) global_facts;
-    val local_facts' = local_facts
-      |> Attrib.partial_evaluation lthy
-      |> Element.transform_facts (Local_Theory.target_morphism lthy);
-  in
-    lthy
-    |> Local_Theory.background_theory (Global_Theory.note_thmss kind global_facts' #> snd)
-    |> Local_Theory.target (Locale.add_thmss locale kind local_facts')
-  end;
-
 fun target_notes (Target {target, is_locale, ...}) =
-  if is_locale then locale_notes target
-  else fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts;
+  if is_locale then Generic_Target.locale_notes target
+  else Generic_Target.theory_notes;
 
 
 (* abbrev *)
@@ -145,8 +133,9 @@
     lthy
     |> pervasive ? Generic_Target.background_declaration decl
     |> Generic_Target.locale_declaration target syntax decl
-    |> (fn lthy' => lthy' |> Local_Theory.map_contexts (fn level => fn ctxt => ctxt |>
-        level > 0 ? Context.proof_map (Local_Theory.standard_form lthy' ctxt decl)));
+    |> (fn lthy' => lthy' |> Local_Theory.map_contexts (fn level => fn ctxt =>
+        if level = 0 then ctxt
+        else Context.proof_map (Local_Theory.standard_form lthy' ctxt decl) ctxt));
 
 
 (* pretty *)
diff -r c0481c3c2a6c -r 6523a21076a8 src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Sun Apr 01 19:07:32 2012 +0200
+++ b/src/Pure/Isar/overloading.ML	Sun Apr 01 20:36:33 2012 +0200
@@ -203,8 +203,7 @@
     |> synchronize_syntax
     |> Local_Theory.init naming
        {define = Generic_Target.define foundation,
-        notes = Generic_Target.notes
-          (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
+        notes = Generic_Target.notes Generic_Target.theory_notes,
         abbrev = Generic_Target.abbrev
           (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
             Generic_Target.theory_abbrev prmode ((b, mx), t)),