1.1 --- a/test/Tools/isac/BaseDefinitions/kestore.sml	Sat Aug 06 10:45:24 2022 +0200
     1.2 +++ b/test/Tools/isac/BaseDefinitions/kestore.sml	Sat Aug 06 15:02:55 2022 +0200
     1.3 @@ -33,7 +33,6 @@
     1.4  "-------- fun Test_KEStore_Elems.add_rlss overwrites earlier data -----------------";
     1.5  "-------- fun Test_KEStore_Elems.add_rlss overwrites earlier data -----------------";
     1.6  "-------- fun Test_KEStore_Elems.add_rlss overwrites earlier data -----------------";
     1.7 -  fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
     1.8    fun rls_eq ((id1, (thyID1, _)), (id2, (thyID2, _))) = id1 = id2 (*andalso thyID1 = thyID2*)
     1.9  
    1.10  val data1 = [("test", ("theory-1", Rule_Set.Empty)),
    1.11 @@ -43,7 +42,7 @@
    1.12    [("test_rls", ("theory-2",
    1.13      Rule_Set.append_rules "test_rls" Rule_Set.empty [Thm ("not_def", @{thm not_def})]))]
    1.14  val data_3a = union rls_eq data1 data2
    1.15 -val data_3b = union_overwrite rls_eq data1 data2
    1.16 +val data_3b = Library.merge rls_eq (data1, data2)
    1.17  
    1.18  val SOME (_, Rule_Set.Repeat {rules, ...}) = AList.lookup op = data_3a "test_rls";
    1.19  case rules of
    1.20 @@ -53,9 +52,9 @@
    1.21  val SOME (_, Rule_Set.Repeat {rules, ...}) = AList.lookup op = data_3b "test_rls";
    1.22  case rules of
    1.23    [Thm ("refl", _), Thm ("subst", _)] => ()
    1.24 -| _ => error "union_overwrite rls_eq changed: 2nd argument is NOT overwritten anymore"
    1.25 +| _ => error "Library.merge rls_eq changed: 2nd argument is NOT overwritten anymore"
    1.26  
    1.27 -(* add_rlss will take union_overwrite due to argument sequence *)
    1.28 +(* add_rlss will take Library.merge due to argument sequence *)
    1.29  
    1.30  
    1.31  "-------- ERROR assoc_calc: 'Prog_Expr.is_num' not found in theory Poly ------";
    1.32 @@ -87,7 +86,7 @@
    1.33  val calcs = 
    1.34         KEStore_Elems.get_calcs thy;
    1.35  
    1.36 -(*+*)val ("is_polyrat_in", ("Poly.is_polyrat_in", _)) = nth 17 calcs; (* <<<<<------- is_atom <> is_num *)
    1.37 +(*+*)val ("matches", ("Prog_Expr.matches", _)) = nth 17 calcs;
    1.38  (*+*)map fst calcs = (*..WITH declare [[ML_print_depth = 999]]*)
    1.39     ["Test.precond_rootmet", "contains_root", "Test.precond_rootpbl", "is_f_x", "primed", "is_normSqrtTerm_in", "is_rootTerm_in", "SQRT", "is_sqrtTerm_in", "is_ratequation_in", "is_rootRatAddTerm_in", "add_new_c",
    1.40      "occur_exactly_in", "is_addUnordered", "is_polyexp", "is_poly_in", "is_polyrat_in", "POWER", "TIMES", "PLUS", "ident", "le", "is_atom", "occurs_in", "is_num", "matchsub", "Vars", "lhs", "rhs", "matches",