tuned signature;

--- a/src/Pure/Isar/element.ML	Sun Nov 20 17:44:41 2011 +0100
+++ b/src/Pure/Isar/element.ML	Sun Nov 20 17:57:09 2011 +0100
@@ -20,15 +20,15 @@
     Notes of string * (Attrib.binding * ('fact * Attrib.src list) list) list
   type context = (string, string, Facts.ref) ctxt
   type context_i = (typ, term, thm list) ctxt
-  val facts_map: (('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt) ->
-   (Attrib.binding * ('fact * Attrib.src list) list) list ->
-   (Attrib.binding * ('c * Attrib.src list) list) list
   val map_ctxt: {binding: binding -> binding, typ: 'typ -> 'a, term: 'term -> 'b,
     pattern: 'term -> 'b, fact: 'fact -> 'c, attrib: Attrib.src -> Attrib.src} ->
     ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt
   val map_ctxt_attrib: (Attrib.src -> Attrib.src) ->
     ('typ, 'term, 'fact) ctxt -> ('typ, 'term, 'fact) ctxt
   val transform_ctxt: morphism -> context_i -> context_i
+  val transform_facts: morphism ->
+    (Attrib.binding * (thm list * Args.src list) list) list ->
+    (Attrib.binding * (thm list * Args.src list) list) list
   val pretty_stmt: Proof.context -> statement_i -> Pretty.T list
   val pretty_ctxt: Proof.context -> context_i -> Pretty.T list
   val pretty_statement: Proof.context -> string -> thm -> Pretty.T
@@ -85,8 +85,6 @@
 type context = (string, string, Facts.ref) ctxt;
 type context_i = (typ, term, thm list) ctxt;
 
-fun facts_map f facts = Notes ("", facts) |> f |> (fn Notes (_, facts') => facts');
-
 fun map_ctxt {binding, typ, term, pattern, fact, attrib} =
   fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) => (binding x, Option.map typ T, mx)))
    | Constrains xs => Constrains (xs |> map (fn (x, T) =>
@@ -109,6 +107,9 @@
   fact = Morphism.fact phi,
   attrib = Args.transform_values phi};
 
+fun transform_facts phi facts =
+  Notes ("", facts) |> transform_ctxt phi |> (fn Notes (_, facts') => facts');
+
 
 
 (** pretty printing **)

--- a/src/Pure/Isar/locale.ML	Sun Nov 20 17:44:41 2011 +0100
+++ b/src/Pure/Isar/locale.ML	Sun Nov 20 17:57:09 2011 +0100
@@ -426,8 +426,7 @@
           (case export' of
             NONE => Morphism.identity
           | SOME export => collect_mixins context (name, morph $> export) $> export);
-        val facts' = facts
-          |> Element.facts_map (Element.transform_ctxt (transfer input $> morph $> mixin));
+        val facts' = facts |> Element.transform_facts (transfer input $> morph $> mixin);
       in activ_elem (Notes (kind, facts')) input end;
   in
     fold_rev activate notes input
@@ -567,7 +566,7 @@
       (fn thy => fold_rev (fn (_, morph) =>
             let
               val facts' = facts
-                |> Element.facts_map (Element.transform_ctxt morph)
+                |> Element.transform_facts morph
                 |> Attrib.map_facts (map (Attrib.attribute_i thy));
             in snd o Global_Theory.note_thmss kind facts' end)
         (registrations_of (Context.Theory thy) loc) thy));

--- a/src/Pure/Isar/named_target.ML	Sun Nov 20 17:44:41 2011 +0100
+++ b/src/Pure/Isar/named_target.ML	Sun Nov 20 17:57:09 2011 +0100
@@ -120,7 +120,7 @@
     val global_facts' = Attrib.map_facts (K []) global_facts;
     val local_facts' = local_facts
       |> Attrib.partial_evaluation lthy
-      |> Element.facts_map (Element.transform_ctxt (Local_Theory.target_morphism lthy));
+      |> Element.transform_facts (Local_Theory.target_morphism lthy);
   in
     lthy
     |> Local_Theory.background_theory (Global_Theory.note_thmss kind global_facts' #> snd)

--- a/src/Pure/Isar/specification.ML	Sun Nov 20 17:44:41 2011 +0100
+++ b/src/Pure/Isar/specification.ML	Sun Nov 20 17:57:09 2011 +0100
@@ -298,7 +298,7 @@
 
     val facts' = facts
       |> Attrib.partial_evaluation ctxt'
-      |> Element.facts_map (Element.transform_ctxt (Proof_Context.export_morphism ctxt' lthy));
+      |> Element.transform_facts (Proof_Context.export_morphism ctxt' lthy);
     val (res, lthy') = lthy |> Local_Theory.notes_kind kind facts';
     val _ = Proof_Display.print_results int lthy' ((kind, ""), res);
   in (res, lthy') end;