1.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_All.thy Mon Jan 27 13:40:36 2014 +0100
1.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_All.thy Mon Jan 27 21:49:27 2014 +0100
1.3 @@ -1,7 +1,7 @@
1.4 theory Thy_All imports Thy_3 Thy_5 begin
1.5
1.6 ML {*
1.7 -KEStore_Elems.get_rlss @{theory}
1.8 +Test_KEStore_Elems.get_rlss @{theory}
1.9 (*|> map check_kestore_rls
1.10 |> enumerate_strings
1.11 |> map writeln*)
1.12 @@ -12,13 +12,13 @@
1.13 (test_list_rls, (Thy_3, Rls {#calc = 0, #rules = 1, ...))--4
1.14 *)
1.15 ;
1.16 -case KEStore_Elems.get_rlss @{theory} of
1.17 +case Test_KEStore_Elems.get_rlss @{theory} of
1.18 ("rls2", ("Thy_4", Erls)) :: ("rls1", ("Thy_4", Erls)) :: _ => ()
1.19 -| _ => raise error "KEStore_Elems.get_rlss changed"
1.20 +| _ => raise error "Test_KEStore_Elems.get_rlss changed"
1.21 ;
1.22 -case KEStore_Elems.get_calcs @{theory} of
1.23 +case Test_KEStore_Elems.get_calcs @{theory} of
1.24 [("calc", ("Thy_1", _))] => ()
1.25 -| _ => raise error "KEStore_Elems.get_calcs changed"
1.26 +| _ => raise error "Test_KEStore_Elems.get_calcs changed"
1.27 *}
1.28
1.29 end