1.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_3.thy	Mon Jan 27 13:40:36 2014 +0100
     1.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_3.thy	Mon Jan 27 21:49:27 2014 +0100
     1.3 @@ -3,27 +3,27 @@
     1.4  ML {* val test_list_rls =
     1.5    append_rls "test_list_rls" e_rls [Thm ("not_def", @{thm not_def})] *}
     1.6  
     1.7 -setup {* KEStore_Elems.add_rlss (*already added in Thy_1.thy and Thy_2.thy*)
     1.8 +setup {* Test_KEStore_Elems.add_rlss (*already added in Thy_1.thy and Thy_2.thy*)
     1.9    [("test_list_rls", (Context.theory_name @{theory}, test_list_rls))] *}
    1.10  
    1.11  ML {*
    1.12 -  if length (KEStore_Elems.get_rlss @{theory}) = 1 (*stored in 3 different theories*)
    1.13 +  if length (Test_KEStore_Elems.get_rlss @{theory}) = 1 (*stored in 3 different theories*)
    1.14    then () else error "rls identified by string-identifier, not by theory: changed"
    1.15  
    1.16  (*test_ruleset' := overwritelthy @{theory} (! test_ruleset', [("test_list_rls", 
    1.17      append_rls "test_list_rls" test_list_rls [Calc ("test_function", e_evalfn)])])*)
    1.18    ;
    1.19 -(*if length (KEStore_Elems.get_rlss @{theory}) = length (! test_ruleset')
    1.20 -  then () else error "KEStore_Elems.get_rlss = test_ruleset': changed"*)
    1.21 +(*if length (Test_KEStore_Elems.get_rlss @{theory}) = length (! test_ruleset')
    1.22 +  then () else error "Test_KEStore_Elems.get_rlss = test_ruleset': changed"*)
    1.23    ;
    1.24    val SOME (_, Rls {rules, ...}) =
    1.25 -    AList.lookup op= (KEStore_Elems.get_rlss @{theory}) "test_list_rls"
    1.26 +    AList.lookup op= (Test_KEStore_Elems.get_rlss @{theory}) "test_list_rls"
    1.27    ;
    1.28    case rules of
    1.29      [Thm ("not_def", _)] => ()
    1.30    | _ => error "union rls_eq changed: 1st argument is NOT overwritten anymore"
    1.31    (* merge rules of rls with the same identifier rls' must be done one level higher:
    1.32 -    KEStore_Elems.add_rlss does *add* or *overwrite* *)
    1.33 +    Test_KEStore_Elems.add_rlss does *add* or *overwrite* *)
    1.34  *}
    1.35  
    1.36  end