test/Tools/isac/kestore.sml
changeset 55359 73dc85c025ab
parent 52139 511fc271f783
child 55397 71f7fd375e7d
     1.1 --- a/test/Tools/isac/kestore.sml	Mon Jan 27 13:40:36 2014 +0100
     1.2 +++ b/test/Tools/isac/kestore.sml	Mon Jan 27 21:49:27 2014 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  "table of contents -----------------------------------------------------------";
     1.5  "-----------------------------------------------------------------------------";
     1.6  "-------- fun check_kestore_rls ----------------------------------------------";
     1.7 -"-------- fun KEStore_Elems.add_rlss overwrites earlier data -----------------";
     1.8 +"-------- fun Test_KEStore_Elems.add_rlss overwrites earlier data ------------";
     1.9  "-----------------------------------------------------------------------------";
    1.10  "-----------------------------------------------------------------------------";
    1.11  
    1.12 @@ -19,16 +19,16 @@
    1.13    "(e_rls, (KEStore, Rls {#calc = 0, #rules = 0, ...))"
    1.14  then () else error "check_kestore_rls changed"
    1.15  ;
    1.16 -KEStore_Elems.get_rlss @{theory Isac} 
    1.17 +Test_KEStore_Elems.get_rlss @{theory Isac} 
    1.18    |> map check_kestore_rls 
    1.19    |> enumerate_strings
    1.20    |> sort string_ord
    1.21  (*|> map writeln*)
    1.22  ;
    1.23  
    1.24 -"-------- fun KEStore_Elems.add_rlss overwrites earlier data -----------------";
    1.25 -"-------- fun KEStore_Elems.add_rlss overwrites earlier data -----------------";
    1.26 -"-------- fun KEStore_Elems.add_rlss overwrites earlier data -----------------";
    1.27 +"-------- fun Test_KEStore_Elems.add_rlss overwrites earlier data -----------------";
    1.28 +"-------- fun Test_KEStore_Elems.add_rlss overwrites earlier data -----------------";
    1.29 +"-------- fun Test_KEStore_Elems.add_rlss overwrites earlier data -----------------";
    1.30    fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
    1.31    fun rls_eq ((id1, (thyID1, _)), (id2, (thyID2, _))) = id1 = id2 (*andalso thyID1 = thyID2*)
    1.32