1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Sat Aug 06 10:45:24 2022 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Sat Aug 06 15:02:55 2022 +0200
     1.3 @@ -91,8 +91,6 @@
     1.4  
     1.5  structure KEStore_Elems(**): KESTORE_ELEMS(**) =
     1.6  struct
     1.7 -  fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
     1.8 -
     1.9    structure Data = Theory_Data (
    1.10      type T = (string * (LibraryC.subst -> term * term -> bool)) list;
    1.11      val empty = [];
    1.12 @@ -100,7 +98,7 @@
    1.13      val merge = merge Rewrite_Ord.equal;
    1.14      );  
    1.15    fun get_rew_ord thy = Data.get thy
    1.16 -  fun add_rew_ord rlss = Data.map (union_overwrite Rewrite_Ord.equal rlss)
    1.17 +  fun add_rew_ord rlss = Data.map (curry (Library.merge Rewrite_Ord.equal) rlss)
    1.18  
    1.19    structure Data = Theory_Data (
    1.20      type T = (Rule_Set.id * (ThyC.id * Rule_Set.T)) list;
    1.21 @@ -109,7 +107,7 @@
    1.22      val merge = Rule_Set.to_kestore;
    1.23      );  
    1.24    fun get_rlss thy = Data.get thy
    1.25 -  fun add_rlss rlss = Data.map (union_overwrite Rule_Set.equal rlss)
    1.26 +  fun add_rlss rlss = Data.map (curry (Library.merge Rule_Set.equal) rlss)
    1.27  
    1.28    structure Data = Theory_Data (
    1.29      type T = (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list;
    1.30 @@ -118,7 +116,7 @@
    1.31      val merge = merge Eval_Def.calc_eq;
    1.32      );                                                              
    1.33    fun get_calcs thy = Data.get thy
    1.34 -  fun add_calcs calcs = Data.map (union_overwrite Eval_Def.calc_eq calcs)
    1.35 +  fun add_calcs calcs = Data.map (curry (Library.merge Eval_Def.calc_eq) calcs)
    1.36  
    1.37    structure Data = Theory_Data (
    1.38      type T = (term * (References_Def.T * (term list -> (term * term list) list))) list;
    1.39 @@ -127,7 +125,7 @@
    1.40      val merge = merge CAS_Def.equal;
    1.41      );                                                              
    1.42    fun get_cas thy = Data.get thy
    1.43 -  fun add_cas cas = Data.map (union_overwrite CAS_Def.equal cas)
    1.44 +  fun add_cas cas = Data.map (curry (Library.merge CAS_Def.equal) cas)
    1.45  
    1.46    structure Data = Theory_Data (
    1.47      type T = Probl_Def.store;
    1.48 @@ -358,6 +356,23 @@
    1.49  \<close>
    1.50  ML \<open>
    1.51  \<close> ML \<open>
    1.52 +  fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
    1.53 +\<close> ML \<open>
    1.54 +union_overwrite: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list;
    1.55 +merge          : ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
    1.56 +\<close> ML \<open>
    1.57 +val eq = op=;
    1.58 +val l1 = [1,2,3,4,5];
    1.59 +val l2 = [4,5,6,7,8];
    1.60 +\<close> ML \<open>
    1.61 +union_overwrite eq l1 l2  = [8, 7, 6, 1, 2, 3, 4, 5];
    1.62 +Library.merge eq (l1, l2) = [6, 7, 8, 1, 2, 3, 4, 5]
    1.63 +\<close> ML \<open>
    1.64 +\<close> ML \<open>
    1.65 +Library.merge eq        (*: _a list * _a list -> _a list*);
    1.66 +curry (Library.merge eq)(*: _a list -> _a list -> _a list*)
    1.67 +\<close> ML \<open>
    1.68 +\<close> ML \<open>
    1.69  \<close> ML \<open>
    1.70  \<close>
    1.71  end