# HG changeset patch
# User wenzelm
# Date 1333300052 -7200
# Node ID c0481c3c2a6cffa71036032887a09957a561d6a4
# Parent  afacccb4e2c7d0f2265ce08d8bda551aeec20cb4
added Attrib.global_notes/local_notes/generic_notes convenience;

diff -r afacccb4e2c7 -r c0481c3c2a6c src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sun Apr 01 19:04:52 2012 +0200
+++ b/src/Pure/Isar/attrib.ML	Sun Apr 01 19:07:32 2012 +0200
@@ -25,6 +25,12 @@
   val map_facts_refs: ('a list -> 'att list) -> ('b -> 'fact) ->
     (('c * 'a list) * ('b * 'a list) list) list ->
     (('c * 'att list) * ('fact * 'att list) list) list
+  val global_notes: string -> (binding * (thm list * src list) list) list ->
+    theory -> (string * thm list) list * theory
+  val local_notes: string -> (binding * (thm list * src list) list) list ->
+    Proof.context -> (string * thm list) list * Proof.context
+  val generic_notes: string -> (binding * (thm list * src list) list) list ->
+    Context.generic -> (string * thm list) list * Context.generic
   val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
   val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
   val attribute_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
@@ -138,6 +144,15 @@
 
 (* fact expressions *)
 
+fun global_notes kind facts thy = thy |>
+  Global_Theory.note_thmss kind (map_facts (map (attribute_i thy)) facts);
+
+fun local_notes kind facts ctxt = ctxt |>
+  Proof_Context.note_thmss kind (map_facts (map (attribute_i (Proof_Context.theory_of ctxt))) facts);
+
+fun generic_notes kind facts context = context |>
+  Context.mapping_result (global_notes kind facts) (local_notes kind facts);
+
 fun eval_thms ctxt srcs = ctxt
   |> Proof_Context.note_thmss ""
     (map_facts_refs (map (attribute (Proof_Context.theory_of ctxt))) (Proof_Context.get_fact ctxt)
diff -r afacccb4e2c7 -r c0481c3c2a6c src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Sun Apr 01 19:04:52 2012 +0200
+++ b/src/Pure/Isar/bundle.ML	Sun Apr 01 19:07:32 2012 +0200
@@ -87,11 +87,8 @@
 local
 
 fun gen_includes prep args ctxt =
-  let
-    val decls = maps (the_bundle ctxt o prep ctxt) args;
-    val attrib = Attrib.attribute_i (Proof_Context.theory_of ctxt);
-    val note = ((Binding.empty, []), map (apsnd (map attrib)) decls);
-  in #2 (Proof_Context.note_thmss "" [note] ctxt) end;
+  let val decls = maps (the_bundle ctxt o prep ctxt) args
+  in #2 (Attrib.local_notes "" [((Binding.empty, []), decls)] ctxt) end;
 
 fun gen_context prep args (Context.Theory thy) =
       Named_Target.theory_init thy
diff -r afacccb4e2c7 -r c0481c3c2a6c src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Sun Apr 01 19:04:52 2012 +0200
+++ b/src/Pure/Isar/element.ML	Sun Apr 01 19:07:32 2012 +0200
@@ -51,8 +51,6 @@
   val satisfy_morphism: witness list -> morphism
   val eq_morphism: theory -> thm list -> morphism option
   val transfer_morphism: theory -> morphism
-  val generic_note_thmss: string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
-    Context.generic -> (string * thm list) list * Context.generic
   val init: context_i -> Context.generic -> Context.generic
   val activate_i: context_i -> Proof.context -> context_i * Proof.context
   val activate: (typ, term, Facts.ref) ctxt -> Proof.context -> context_i * Proof.context
@@ -483,16 +481,6 @@
 
 (* init *)
 
-fun generic_note_thmss kind facts context =
-  let
-    val facts' =
-      Attrib.map_facts (map (Attrib.attribute_i (Context.theory_of context))) facts;
-  in
-    context |> Context.mapping_result
-      (Global_Theory.note_thmss kind facts')
-      (Proof_Context.note_thmss kind facts')
-  end;
-
 fun init (Fixes fixes) = Context.map_proof (Proof_Context.add_fixes fixes #> #2)
   | init (Constrains _) = I
   | init (Assumes asms) = Context.map_proof (fn ctxt =>
@@ -514,7 +502,7 @@
           |> fold Variable.auto_fixes (map #1 asms)
           |> Proof_Context.add_assms_i Local_Defs.def_export (map #2 asms);
       in ctxt' end)
-  | init (Notes (kind, facts)) = generic_note_thmss kind facts #> #2;
+  | init (Notes (kind, facts)) = Attrib.generic_notes kind facts #> #2;
 
 
 (* activate *)
diff -r afacccb4e2c7 -r c0481c3c2a6c src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Sun Apr 01 19:04:52 2012 +0200
+++ b/src/Pure/Isar/expression.ML	Sun Apr 01 19:07:32 2012 +0200
@@ -816,7 +816,7 @@
 local
 
 fun note_eqns_register deps witss attrss eqns export export' =
-  Element.generic_note_thmss Thm.lemmaK
+  Attrib.generic_notes Thm.lemmaK
     (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns)
   #-> (fn facts => `(fn context => meta_rewrite (Context.proof_of context) (maps snd facts)))
   #-> (fn eqns => fold (fn ((dep, morph), wits) =>
@@ -885,12 +885,10 @@
 
 fun note_eqns_dependency target deps witss attrss eqns export export' ctxt =
   let
-    val thy = Proof_Context.theory_of ctxt;
-
     val facts =
       (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns);
     val eqns' = ctxt
-      |> Proof_Context.note_thmss Thm.lemmaK (Attrib.map_facts (map (Attrib.attribute_i thy)) facts)
+      |> Attrib.local_notes Thm.lemmaK facts
       |-> (fn facts => `(fn ctxt => meta_rewrite ctxt (maps snd facts)))
       |> fst;  (* FIXME duplication to add_thmss *)
   in
diff -r afacccb4e2c7 -r c0481c3c2a6c src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Sun Apr 01 19:04:52 2012 +0200
+++ b/src/Pure/Isar/generic_target.ML	Sun Apr 01 19:07:32 2012 +0200
@@ -142,7 +142,6 @@
 
 fun notes target_notes kind facts lthy =
   let
-    val thy = Proof_Context.theory_of lthy;
     val facts' = facts
       |> map (fn (a, bs) => (a, Global_Theory.burrow_fact (Global_Theory.name_multi
           (Local_Theory.full_name lthy (fst a))) bs))
@@ -152,7 +151,7 @@
   in
     lthy
     |> target_notes kind global_facts local_facts
-    |> Proof_Context.note_thmss kind (Attrib.map_facts (map (Attrib.attribute_i thy)) local_facts)
+    |> Attrib.local_notes kind local_facts
   end;
 
 
@@ -215,15 +214,9 @@
           (Thm.def_binding_optional b b_def, Logic.mk_equals (lhs, rhs)));
   in ((lhs, def), lthy3) end;
 
-fun theory_notes kind global_facts lthy =
-  let
-    val thy = Proof_Context.theory_of lthy;
-    val global_facts' = Attrib.map_facts (map (Attrib.attribute_i thy)) global_facts;
-  in
-    lthy
-    |> Local_Theory.background_theory (Global_Theory.note_thmss kind global_facts' #> snd)
-    |> Local_Theory.target (Proof_Context.note_thmss kind global_facts' #> snd)
-  end;
+fun theory_notes kind global_facts =
+  Local_Theory.background_theory (Attrib.global_notes kind global_facts #> snd) #>
+  Local_Theory.target (Attrib.local_notes kind global_facts #> snd);
 
 fun theory_abbrev prmode ((b, mx), t) =
   Local_Theory.background_theory
diff -r afacccb4e2c7 -r c0481c3c2a6c src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sun Apr 01 19:04:52 2012 +0200
+++ b/src/Pure/Isar/locale.ML	Sun Apr 01 19:07:32 2012 +0200
@@ -535,18 +535,13 @@
 fun add_thmss _ _ [] ctxt = ctxt
   | add_thmss loc kind facts ctxt =
       ctxt
-      |> Proof_Context.note_thmss kind
-        (Attrib.map_facts (map (Attrib.attribute_i (Proof_Context.theory_of ctxt))) facts)
-      |> snd
+      |> Attrib.local_notes kind facts |> snd
       |> Proof_Context.background_theory
         ((change_locale loc o apfst o apsnd) (cons ((kind, facts), serial ())) #>
           (* Registrations *)
-          (fn thy => fold_rev (fn (_, morph) =>
-                let
-                  val facts' = facts
-                    |> Element.transform_facts morph
-                    |> Attrib.map_facts (map (Attrib.attribute_i thy));
-                in snd o Global_Theory.note_thmss kind facts' end)
+          (fn thy =>
+            fold_rev (fn (_, morph) =>
+              snd o Attrib.global_notes kind (Element.transform_facts morph facts))
             (registrations_of (Context.Theory thy) loc) thy));
 
 
diff -r afacccb4e2c7 -r c0481c3c2a6c src/Tools/interpretation_with_defs.ML
--- a/src/Tools/interpretation_with_defs.ML	Sun Apr 01 19:04:52 2012 +0200
+++ b/src/Tools/interpretation_with_defs.ML	Sun Apr 01 19:07:32 2012 +0200
@@ -23,7 +23,7 @@
       map (Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def) o
         maps snd;
   in
-    Element.generic_note_thmss Thm.lemmaK
+    Attrib.generic_notes Thm.lemmaK
       (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns)
     #-> (fn facts => `(fn context => meta_rewrite context facts))
     #-> (fn eqns => fold (fn ((dep, morph), wits) =>