# HG changeset patch
# User wenzelm
# Date 1565943641 -7200
# Node ID 16e98f89a29c6ef01e24245754bdd8e7a966fbe3
# Parent  33749040b6f87e1ce33104d38491eafe522ec3ff
clarified signature;

diff -r 33749040b6f8 -r 16e98f89a29c src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Fri Aug 16 10:04:47 2019 +0200
+++ b/src/Pure/Isar/generic_target.ML	Fri Aug 16 10:20:41 2019 +0200
@@ -306,6 +306,8 @@
 fun bind_name lthy b =
   (Local_Theory.full_name lthy b, Binding.default_pos_of b);
 
+fun map_facts f = map (apsnd (map (apfst (map f))));
+
 in
 
 fun notes target_notes kind facts lthy =
@@ -313,9 +315,9 @@
     val facts' = facts
       |> map (fn (a, bs) =>
           (a, Global_Theory.burrow_fact (Global_Theory.name_multi (bind_name lthy (fst a))) bs))
-      |> Global_Theory.map_facts (import_export_proof lthy);
-    val local_facts = Global_Theory.map_facts #1 facts';
-    val global_facts = Global_Theory.map_facts #2 facts';
+      |> map_facts (import_export_proof lthy);
+    val local_facts = map_facts #1 facts';
+    val global_facts = map_facts #2 facts';
   in
     lthy
     |> target_notes kind global_facts (Attrib.partial_evaluation lthy local_facts)
diff -r 33749040b6f8 -r 16e98f89a29c src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Fri Aug 16 10:04:47 2019 +0200
+++ b/src/Pure/global_theory.ML	Fri Aug 16 10:20:41 2019 +0200
@@ -16,7 +16,6 @@
   val get_thm: theory -> xstring -> thm
   val transfer_theories: theory -> thm -> thm
   val all_thms_of: theory -> bool -> (string * thm) list
-  val map_facts: ('a -> 'b) -> ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list
   val burrow_fact: ('a list -> 'b list) -> ('a list * 'c) list -> ('b list * 'c) list
   val burrow_facts: ('a list -> 'b list) ->
     ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list
@@ -63,15 +62,16 @@
 );
 
 val facts_of = Data.get;
+fun map_facts f = Data.map f;
 
 fun check_fact thy = Facts.check (Context.Theory thy) (facts_of thy);
 val intern_fact = Facts.intern o facts_of;
 val defined_fact = Facts.defined o facts_of;
 
 fun alias_fact binding name thy =
-  Data.map (Facts.alias (Sign.naming_of thy) binding name) thy;
+  map_facts (Facts.alias (Sign.naming_of thy) binding name) thy;
 
-fun hide_fact fully name = Data.map (Facts.hide fully name);
+fun hide_fact fully name = map_facts (Facts.hide fully name);
 
 
 (* retrieve theorems *)
@@ -106,7 +106,6 @@
 
 (* fact specifications *)
 
-fun map_facts f = map (apsnd (map (apfst (map f))));
 fun burrow_fact f = split_list #>> burrow f #> op ~~;
 fun burrow_facts f = split_list ##> burrow (burrow_fact f) #> op ~~;
 
@@ -176,7 +175,7 @@
         end);
     val arg = (b, Lazy.map_finished (tap check) fact);
   in
-    thy |> Data.map (Facts.add_static (Context.Theory thy) {strict = true, index = false} arg #> #2)
+    thy |> map_facts (Facts.add_static (Context.Theory thy) {strict = true, index = false} arg #> #2)
   end;
 
 fun check_thms_lazy (thms: thm list lazy) =
@@ -231,8 +230,8 @@
 (* dynamic theorems *)
 
 fun add_thms_dynamic' context arg thy =
-  let val (name, facts') = Facts.add_dynamic context arg (Data.get thy)
-  in (name, Data.put facts' thy) end;
+  let val (name, facts') = Facts.add_dynamic context arg (facts_of thy)
+  in (name, map_facts (K facts') thy) end;
 
 fun add_thms_dynamic arg thy =
   add_thms_dynamic' (Context.Theory thy) arg thy |> snd;