1.1 --- a/test/Tools/isac/OLDTESTS/scriptnew.sml	Mon Jan 27 21:58:57 2014 +0100
     1.2 +++ b/test/Tools/isac/OLDTESTS/scriptnew.sml	Mon Jan 27 22:26:51 2014 +0100
     1.3 @@ -19,20 +19,7 @@
     1.4  "  --- test 30.4.02 Testterm:  Repeat Repeat Or ------------------ ";
     1.5  "  --- test 30.4.02 Testterm:  Repeat Repeat Or ------------------ ";
     1.6  "  --- test 30.4.02 Testterm:  Repeat Repeat Or ------------------ ";
     1.7 -store_pbt
     1.8 - (prep_pbt Test.thy "pbl_testss" [] e_pblID
     1.9 - (["tests"],
    1.10 -  []:(string * string list) list,
    1.11 -  e_rls, NONE, []));
    1.12 -store_pbt
    1.13 - (prep_pbt Test.thy "pbl_testss_term" [] e_pblID
    1.14 - (["met_testterm","tests"],
    1.15 -  [("#Given" ,["realTestGiven g_"]),
    1.16 -   ("#Find"  ,["realTestFind f_"])
    1.17 -  ],
    1.18 -  e_rls, NONE, []));
    1.19 -
    1.20 -Test_KEStore_Elems.add_pbts
    1.21 +KEStore_Elems.add_pbts
    1.22    [prep_pbt Test.thy "pbl_testss" [] e_pblID
    1.23        (["tests"], []:(string * string list) list, e_rls, NONE, []),
    1.24      prep_pbt Test.thy "pbl_testss_term" [] e_pblID
    1.25 @@ -102,14 +89,7 @@
    1.26  "  --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ ";
    1.27  "  --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ ";
    1.28  "  --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ ";
    1.29 -store_pbt
    1.30 - (prep_pbt Test.thy "pbl_testss_eq" [] e_pblID
    1.31 - (["met_testeq","tests"],
    1.32 -  [("#Given" ,["boolTestGiven e_e"]),
    1.33 -   ("#Find"  ,["boolTestFind v_i_"])
    1.34 -  ],
    1.35 -  e_rls, NONE, []));
    1.36 -Test_KEStore_Elems.add_pbts
    1.37 +KEStore_Elems.add_pbts
    1.38    [prep_pbt Test.thy "pbl_testss_eq" [] e_pblID
    1.39        (["met_testeq","tests"],
    1.40          [("#Given" ,["boolTestGiven e_e"]),