1.1 --- a/test/Tools/isac/CalcElements/kestore.sml	Sat Apr 04 12:11:32 2020 +0200
     1.2 +++ b/test/Tools/isac/CalcElements/kestore.sml	Mon Apr 06 11:44:36 2020 +0200
     1.3 @@ -32,7 +32,7 @@
     1.4    fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
     1.5    fun rls_eq ((id1, (thyID1, _)), (id2, (thyID2, _))) = id1 = id2 (*andalso thyID1 = thyID2*)
     1.6  
     1.7 -val data1 = [("test", ("theory-1", Erls)),
     1.8 +val data1 = [("test", ("theory-1", Rule_Set.Empty)),
     1.9    ("test_rls", ("theory-1", 
    1.10      append_rls "test_rls" e_rls [Thm ("refl", @{thm refl}), Thm ("subst", @{thm subst})]))]
    1.11  val data2 = 
    1.12 @@ -41,12 +41,12 @@
    1.13  val data_3a = union rls_eq data1 data2
    1.14  val data_3b = union_overwrite rls_eq data1 data2
    1.15  
    1.16 -val SOME (_, Rls {rules, ...}) = AList.lookup op = data_3a "test_rls";
    1.17 +val SOME (_, Rule_Set.Repeat {rules, ...}) = AList.lookup op = data_3a "test_rls";
    1.18  case rules of
    1.19    [Thm ("not_def", _)] => ()
    1.20  | _ => error "union rls_eq changed: 1st argument is NOT overwritten anymore"
    1.21  ;
    1.22 -val SOME (_, Rls {rules, ...}) = AList.lookup op = data_3b "test_rls";
    1.23 +val SOME (_, Rule_Set.Repeat {rules, ...}) = AList.lookup op = data_3b "test_rls";
    1.24  case rules of
    1.25    [Thm ("refl", _), Thm ("subst", _)] => ()
    1.26  | _ => error "union_overwrite rls_eq changed: 2nd argument is NOT overwritten anymore"