1.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_1.thy Mon Jan 27 13:40:36 2014 +0100
1.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_1.thy Mon Jan 27 21:49:27 2014 +0100
1.3 @@ -1,19 +1,19 @@
1.4 theory Thy_1 imports Lucas_Interpreter begin
1.5
1.6 ML {*
1.7 - (* CHECK length (KEStore_Elems.get_rlss @{theory}) = length (! ruleset')
1.8 + (* CHECK length (Test_KEStore_Elems.get_rlss @{theory}) = length (! ruleset')
1.9 AT THE BOTTOM OF A THEORY:*)
1.10 - length (KEStore_Elems.get_rlss @{theory}) = 0;
1.11 + length (Test_KEStore_Elems.get_rlss @{theory}) = 0;
1.12 (*length (! test_ruleset') = 1 (* if you have clicked somewhere below *)*)
1.13 *}
1.14 -setup {* KEStore_Elems.add_rlss [("test_list_rls", (Context.theory_name @{theory}, Erls))] *}
1.15 +setup {* Test_KEStore_Elems.add_rlss [("test_list_rls", (Context.theory_name @{theory}, Erls))] *}
1.16 ML {*
1.17 (*test_ruleset' := overwritelthy @{theory} (! test_ruleset', [("test_list_rls", Erls)])
1.18 ;
1.19 - if length (KEStore_Elems.get_rlss @{theory}) = length (! test_ruleset') then ()
1.20 - else error "removal of Unsynchonized.ref: ruleset' <> KEStore_Elems.get_rlss in Thy_1"*)
1.21 + if length (Test_KEStore_Elems.get_rlss @{theory}) = length (! test_ruleset') then ()
1.22 + else error "removal of Unsynchonized.ref: ruleset' <> Test_KEStore_Elems.get_rlss in Thy_1"*)
1.23 *}
1.24
1.25 -setup {* KEStore_Elems.add_calcs [("calc", ("Thy_1", e_evalfn))] *}
1.26 +setup {* Test_KEStore_Elems.add_calcs [("calc", ("Thy_1", e_evalfn))] *}
1.27
1.28 end