1.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_3.thy	Mon Apr 06 11:44:36 2020 +0200
     1.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_3.thy	Wed Apr 08 12:32:51 2020 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  theory Thy_3 imports Thy_2 Thy_2b begin
     1.5  
     1.6  ML \<open>val test_list_rls =
     1.7 -  Rule_Set.append_rls "test_list_rls" Rule_Set.e_rls [Rule.Thm ("not_def", @{thm not_def})]\<close>
     1.8 +  Rule_Set.append_rules "test_list_rls" Rule_Set.empty [Rule.Thm ("not_def", @{thm not_def})]\<close>
     1.9  
    1.10  setup \<open>Test_KEStore_Elems.add_rlss (*already added in Thy_1.thy and Thy_2.thy*)
    1.11    [("test_list_rls", (Context.theory_name @{theory}, test_list_rls))]\<close>
    1.12 @@ -11,7 +11,7 @@
    1.13    then () else error "rls identified by string-identifier, not by theory: changed"
    1.14  
    1.15  (*test_ruleset' := overwritelthy @{theory} (! test_ruleset', [("test_list_rls", 
    1.16 -    append_rls "test_list_rls" test_list_rls [Num_Calc ("test_function", e_evalfn)])])*)
    1.17 +    Rule_Set.append_rules "test_list_rls" test_list_rls [Num_Calc ("test_function", e_evalfn)])])*)
    1.18    ;
    1.19  (*if length (Test_KEStore_Elems.get_rlss @{theory}) = length (! test_ruleset')
    1.20    then () else error "Test_KEStore_Elems.get_rlss = test_ruleset': changed"*)
    1.21 @@ -22,7 +22,7 @@
    1.22    case rules of
    1.23      [Rule.Thm ("not_def", _)] => ()
    1.24    | _ => error "union rls_eq changed: 1st argument is NOT overwritten anymore"
    1.25 -  (* merge rules of rls with the same identifier rls' must be done one level higher:
    1.26 +  (* merge rules of rls with the same Rule_Set.identifier must be done one level higher:
    1.27      Test_KEStore_Elems.add_rlss does *add* or *overwrite* *)
    1.28  \<close>
    1.29