test/Tools/isac/ADDTESTS/accumulate-val/Thy_All.thy
changeset 55359 73dc85c025ab
parent 52146 f47e195af9a3
child 59410 2cbb98890190
     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