clarified signature;
authorwenzelm
Fri Aug 16 10:20:41 2019 +0200 (4 days ago)
changeset 7054416e98f89a29c
parent 70543 33749040b6f8
child 70545 b93ba98e627a
clarified signature;
src/Pure/Isar/generic_target.ML
src/Pure/global_theory.ML
     1.1 --- a/src/Pure/Isar/generic_target.ML	Fri Aug 16 10:04:47 2019 +0200
     1.2 +++ b/src/Pure/Isar/generic_target.ML	Fri Aug 16 10:20:41 2019 +0200
     1.3 @@ -306,6 +306,8 @@
     1.4  fun bind_name lthy b =
     1.5    (Local_Theory.full_name lthy b, Binding.default_pos_of b);
     1.6  
     1.7 +fun map_facts f = map (apsnd (map (apfst (map f))));
     1.8 +
     1.9  in
    1.10  
    1.11  fun notes target_notes kind facts lthy =
    1.12 @@ -313,9 +315,9 @@
    1.13      val facts' = facts
    1.14        |> map (fn (a, bs) =>
    1.15            (a, Global_Theory.burrow_fact (Global_Theory.name_multi (bind_name lthy (fst a))) bs))
    1.16 -      |> Global_Theory.map_facts (import_export_proof lthy);
    1.17 -    val local_facts = Global_Theory.map_facts #1 facts';
    1.18 -    val global_facts = Global_Theory.map_facts #2 facts';
    1.19 +      |> map_facts (import_export_proof lthy);
    1.20 +    val local_facts = map_facts #1 facts';
    1.21 +    val global_facts = map_facts #2 facts';
    1.22    in
    1.23      lthy
    1.24      |> target_notes kind global_facts (Attrib.partial_evaluation lthy local_facts)
     2.1 --- a/src/Pure/global_theory.ML	Fri Aug 16 10:04:47 2019 +0200
     2.2 +++ b/src/Pure/global_theory.ML	Fri Aug 16 10:20:41 2019 +0200
     2.3 @@ -16,7 +16,6 @@
     2.4    val get_thm: theory -> xstring -> thm
     2.5    val transfer_theories: theory -> thm -> thm
     2.6    val all_thms_of: theory -> bool -> (string * thm) list
     2.7 -  val map_facts: ('a -> 'b) -> ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list
     2.8    val burrow_fact: ('a list -> 'b list) -> ('a list * 'c) list -> ('b list * 'c) list
     2.9    val burrow_facts: ('a list -> 'b list) ->
    2.10      ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list
    2.11 @@ -63,15 +62,16 @@
    2.12  );
    2.13  
    2.14  val facts_of = Data.get;
    2.15 +fun map_facts f = Data.map f;
    2.16  
    2.17  fun check_fact thy = Facts.check (Context.Theory thy) (facts_of thy);
    2.18  val intern_fact = Facts.intern o facts_of;
    2.19  val defined_fact = Facts.defined o facts_of;
    2.20  
    2.21  fun alias_fact binding name thy =
    2.22 -  Data.map (Facts.alias (Sign.naming_of thy) binding name) thy;
    2.23 +  map_facts (Facts.alias (Sign.naming_of thy) binding name) thy;
    2.24  
    2.25 -fun hide_fact fully name = Data.map (Facts.hide fully name);
    2.26 +fun hide_fact fully name = map_facts (Facts.hide fully name);
    2.27  
    2.28  
    2.29  (* retrieve theorems *)
    2.30 @@ -106,7 +106,6 @@
    2.31  
    2.32  (* fact specifications *)
    2.33  
    2.34 -fun map_facts f = map (apsnd (map (apfst (map f))));
    2.35  fun burrow_fact f = split_list #>> burrow f #> op ~~;
    2.36  fun burrow_facts f = split_list ##> burrow (burrow_fact f) #> op ~~;
    2.37  
    2.38 @@ -176,7 +175,7 @@
    2.39          end);
    2.40      val arg = (b, Lazy.map_finished (tap check) fact);
    2.41    in
    2.42 -    thy |> Data.map (Facts.add_static (Context.Theory thy) {strict = true, index = false} arg #> #2)
    2.43 +    thy |> map_facts (Facts.add_static (Context.Theory thy) {strict = true, index = false} arg #> #2)
    2.44    end;
    2.45  
    2.46  fun check_thms_lazy (thms: thm list lazy) =
    2.47 @@ -231,8 +230,8 @@
    2.48  (* dynamic theorems *)
    2.49  
    2.50  fun add_thms_dynamic' context arg thy =
    2.51 -  let val (name, facts') = Facts.add_dynamic context arg (Data.get thy)
    2.52 -  in (name, Data.put facts' thy) end;
    2.53 +  let val (name, facts') = Facts.add_dynamic context arg (facts_of thy)
    2.54 +  in (name, map_facts (K facts') thy) end;
    2.55  
    2.56  fun add_thms_dynamic arg thy =
    2.57    add_thms_dynamic' (Context.Theory thy) arg thy |> snd;