1.1 --- a/src/Tools/isac/KEStore.thy	Mon Jan 27 13:40:36 2014 +0100
     1.2 +++ b/src/Tools/isac/KEStore.thy	Mon Jan 27 21:49:27 2014 +0100
     1.3 @@ -26,8 +26,7 @@
     1.4    val get_cas: theory -> cas_elem list
     1.5    val add_cas: cas_elem list -> theory -> theory
     1.6    val get_ptyps: theory -> ptyps
     1.7 -  val store_pbts: (pbt * pblID) list -> theory -> theory
     1.8 -  val add_pbt: (pbt * pblID) -> theory -> theory
     1.9 +  val add_pbts: (pbt * pblID) list -> theory -> theory
    1.10    (*etc*)
    1.11  end;                               
    1.12  
    1.13 @@ -69,13 +68,12 @@
    1.14      val merge = merge_ptyps;
    1.15      );
    1.16    fun get_ptyps thy = Data.get thy;
    1.17 -  fun store_pbts pbts = let
    1.18 -          fun store_pbts' (pbt, pblID) = rev pblID |> insrt pblID pbt;
    1.19 -        in fold store_pbts' pbts |> Data.map end;
    1.20 -  (* the pblID has the leaf-element as first; better readability achieved *)
    1.21 -  fun add_pbt (pbt as {guh,...}, pblID) = 
    1.22 -    (if (!check_guhs_unique) then check_pblguh_unique guh (! ptyps) else ();
    1.23 -    Data.map (insrt pblID pbt (rev pblID)))
    1.24 +  fun add_pbts pbts thy = let
    1.25 +          fun add_pbt (pbt as {guh,...}, pblID) =
    1.26 +                (* the pblID has the leaf-element as first; better readability achieved *)
    1.27 +                (if (!check_guhs_unique) then check_pblguh_unique guh (Data.get thy) else ();
    1.28 +                  rev pblID |> insrt pblID pbt);
    1.29 +        in Data.map (fold add_pbt pbts) thy end;
    1.30  
    1.31    (*etc*)
    1.32  end;
    1.33 @@ -116,10 +114,9 @@
    1.34  
    1.35  fun assoc_cas thy key = assoc (KEStore_Elems.get_cas thy, key);
    1.36  
    1.37 -fun get_ptyps () = ! ptyps 
    1.38 +fun get_ptyps () = ! ptyps;
    1.39  (*SWITCH:
    1.40 -fun get_ptyps () = Thy_Info.get_theory "Build_Knowledge" |> KEStore_Elems.get_ptyps*);
    1.41 -val store_pbts = KEStore_Elems.store_pbts;
    1.42 +fun get_ptyps () = Thy_Info.get_theory "Build_Knowledge" |> KEStore_Elems.get_ptyps*)
    1.43  
    1.44  (*SWITCH: outcomment store_pbt, if all occurrences in src+test have in parallel 
    1.45    SETUP ..* KEStore_Elems.add_pbt (.....) *.. 

     2.1 --- a/src/Tools/isac/Knowledge/AlgEin.thy	Mon Jan 27 13:40:36 2014 +0100
     2.2 +++ b/src/Tools/isac/Knowledge/AlgEin.thy	Mon Jan 27 21:49:27 2014 +0100
     2.3 @@ -55,7 +55,7 @@
     2.4  (* show_ptyps();
     2.5     *)
     2.6  *}
     2.7 -setup {* KEStore_Elems.store_pbts
     2.8 +setup {* KEStore_Elems.add_pbts
     2.9    [(prep_pbt thy "pbl_algein" [] e_pblID (["Berechnung"], [], e_rls, NONE, [])),
    2.10      (prep_pbt thy "pbl_algein_numsym" [] e_pblID
    2.11        (["numerischSymbolische", "Berechnung"],

     3.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy	Mon Jan 27 13:40:36 2014 +0100
     3.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy	Mon Jan 27 21:49:27 2014 +0100
     3.3 @@ -175,7 +175,7 @@
     3.4    [["Equation","fromFunction"]]));
     3.5  KEStore_Elems.get_ptyps @{theory};
     3.6  *}
     3.7 -setup {* KEStore_Elems.store_pbts
     3.8 +setup {* KEStore_Elems.add_pbts
     3.9    [(prep_pbt thy "pbl_bieg" [] e_pblID
    3.10        (["Biegelinien"],
    3.11          [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q"]),

     4.1 --- a/src/Tools/isac/Knowledge/Diff.thy	Mon Jan 27 13:40:36 2014 +0100
     4.2 +++ b/src/Tools/isac/Knowledge/Diff.thy	Mon Jan 27 21:49:27 2014 +0100
     4.3 @@ -272,7 +272,7 @@
     4.4    append_rls "e_rls" e_rls [],
     4.5    SOME "Differentiate (f_f, v_v)", [["diff","differentiate_equality"]]));
     4.6  *}
     4.7 -setup {* KEStore_Elems.store_pbts
     4.8 +setup {* KEStore_Elems.add_pbts
     4.9    [(prep_pbt thy "pbl_fun" [] e_pblID (["function"], [], e_rls, NONE, [])),
    4.10      (prep_pbt thy "pbl_fun_deriv" [] e_pblID
    4.11        (["derivative_of","function"],

     5.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy	Mon Jan 27 13:40:36 2014 +0100
     5.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy	Mon Jan 27 21:49:27 2014 +0100
     5.3 @@ -136,7 +136,7 @@
     5.4    ],
     5.5    e_rls, NONE, []));
     5.6  *}
     5.7 -setup {* KEStore_Elems.store_pbts
     5.8 +setup {* KEStore_Elems.add_pbts
     5.9    [(prep_pbt thy "pbl_fun_max" [] e_pblID
    5.10        (["maximum_of","function"],
    5.11          [("#Given" ,["fixedValues f_ix"]),

     6.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy	Mon Jan 27 13:40:36 2014 +0100
     6.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy	Mon Jan 27 21:49:27 2014 +0100
     6.3 @@ -31,7 +31,7 @@
     6.4    e_rls, SOME "solve (e_e::bool, v_v::int)",
     6.5    [["LinEq","solve_lineq_equation"]])); (*-----TODO*)
     6.6  *}
     6.7 -setup {* KEStore_Elems.store_pbts
     6.8 +setup {* KEStore_Elems.add_pbts
     6.9    [(prep_pbt thy "pbl_equ_dio" [] e_pblID
    6.10        (["diophantine","equation"],
    6.11          [("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),

     7.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy	Mon Jan 27 13:40:36 2014 +0100
     7.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy	Mon Jan 27 21:49:27 2014 +0100
     7.3 @@ -539,7 +539,7 @@
     7.4     *)
     7.5  
     7.6  *}
     7.7 -setup {* KEStore_Elems.store_pbts
     7.8 +setup {* KEStore_Elems.add_pbts
     7.9    [(prep_pbt thy "pbl_equsys" [] e_pblID
    7.10        (["system"],
    7.11          [("#Given" ,["equalities e_s", "solveForVars v_s"]),

     8.1 --- a/src/Tools/isac/Knowledge/Equation.thy	Mon Jan 27 13:40:36 2014 +0100
     8.2 +++ b/src/Tools/isac/Knowledge/Equation.thy	Mon Jan 27 21:49:27 2014 +0100
     8.3 @@ -69,7 +69,7 @@
     8.4    ],
     8.5    univariate_equation_prls,SOME "solve (e_e::bool, v_v)",[]));
     8.6  *}
     8.7 -setup {* KEStore_Elems.store_pbts
     8.8 +setup {* KEStore_Elems.add_pbts
     8.9    [(prep_pbt thy "pbl_equ" [] e_pblID
    8.10        (["equation"],
    8.11          [("#Given" ,["equality e_e","solveFor v_v"]),

     9.1 --- a/src/Tools/isac/Knowledge/InsSort.thy	Mon Jan 27 13:40:36 2014 +0100
     9.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy	Mon Jan 27 21:49:27 2014 +0100
     9.3 @@ -77,7 +77,7 @@
     9.4    ],
     9.5    []));
     9.6  *}
     9.7 -setup {* KEStore_Elems.store_pbts
     9.8 +setup {* KEStore_Elems.add_pbts
     9.9    [(prep_pbt @{theory "InsSort"}
    9.10        (["functional"]:pblID,
    9.11          [("#Given" ,["unsorted u_"]), ("#Find"  ,["sorted s_"])], [])),

    10.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Mon Jan 27 13:40:36 2014 +0100
    10.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Mon Jan 27 21:49:27 2014 +0100
    10.3 @@ -359,7 +359,7 @@
    10.4    [["diff","integration","named"]]));
    10.5   
    10.6  *}
    10.7 -setup {* KEStore_Elems.store_pbts
    10.8 +setup {* KEStore_Elems.add_pbts
    10.9    [(prep_pbt thy "pbl_fun_integ" [] e_pblID
   10.10        (["integrate","function"],
   10.11          [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),

    11.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Mon Jan 27 13:40:36 2014 +0100
    11.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Mon Jan 27 21:49:27 2014 +0100
    11.3 @@ -73,7 +73,7 @@
    11.4      append_rls "e_rls" e_rls [(*for preds in where_*)], NONE, 
    11.5      [["SignalProcessing","Z_Transform","Inverse"]]));
    11.6  *}
    11.7 -setup {* KEStore_Elems.store_pbts
    11.8 +setup {* KEStore_Elems.add_pbts
    11.9    [(prep_pbt thy "pbl_SP" [] e_pblID (["SignalProcessing"], [], e_rls, NONE, [])),
   11.10      (prep_pbt thy "pbl_SP_Ztrans" [] e_pblID
   11.11        (["Z_Transform","SignalProcessing"], [], e_rls, NONE, [])),

    12.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Mon Jan 27 13:40:36 2014 +0100
    12.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Mon Jan 27 21:49:27 2014 +0100
    12.3 @@ -140,7 +140,7 @@
    12.4    LinEq_prls, SOME "solve (e_e::bool, v_v)",
    12.5    [["LinEq","solve_lineq_equation"]]));
    12.6  *}
    12.7 -setup {* KEStore_Elems.store_pbts
    12.8 +setup {* KEStore_Elems.add_pbts
    12.9    [(prep_pbt thy "pbl_equ_univ_lin" [] e_pblID
   12.10        (["LINEAR", "univariate", "equation"],
   12.11          [("#Given" ,["equality e_e", "solveFor v_v"]),

    13.1 --- a/src/Tools/isac/Knowledge/LogExp.thy	Mon Jan 27 13:40:36 2014 +0100
    13.2 +++ b/src/Tools/isac/Knowledge/LogExp.thy	Mon Jan 27 21:49:27 2014 +0100
    13.3 @@ -40,7 +40,7 @@
    13.4    PolyEq_prls, SOME "solve (e_e::bool, v_v)",
    13.5    [["Equation","solve_log"]]));
    13.6  *}
    13.7 -setup {* KEStore_Elems.store_pbts
    13.8 +setup {* KEStore_Elems.add_pbts
    13.9    [(prep_pbt thy "pbl_test_equ_univ_log" [] e_pblID
   13.10        (["logarithmic","univariate","equation"],
   13.11          [("#Given",["equality e_e","solveFor v_v"]),

    14.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy	Mon Jan 27 13:40:36 2014 +0100
    14.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy	Mon Jan 27 21:49:27 2014 +0100
    14.3 @@ -182,7 +182,7 @@
    14.4    NONE, 
    14.5    [["simplification","of_rationals","to_partial_fraction"]]));
    14.6  *}
    14.7 -setup {* KEStore_Elems.store_pbts
    14.8 +setup {* KEStore_Elems.add_pbts
    14.9    [(prep_pbt @{theory} "pbl_simp_rat_partfrac" [] e_pblID
   14.10        (["partial_fraction", "rational", "simplification"],
   14.11          [("#Given" ,["functionTerm t_t", "solveFor v_v"]),

    15.1 --- a/src/Tools/isac/Knowledge/Poly.thy	Mon Jan 27 13:40:36 2014 +0100
    15.2 +++ b/src/Tools/isac/Knowledge/Poly.thy	Mon Jan 27 21:49:27 2014 +0100
    15.3 @@ -1607,7 +1607,7 @@
    15.4    SOME "Simplify t_t", 
    15.5    [["simplification","for_polynomials"]]));
    15.6  *}
    15.7 -setup {* KEStore_Elems.store_pbts
    15.8 +setup {* KEStore_Elems.add_pbts
    15.9    [(prep_pbt thy "pbl_simp_poly" [] e_pblID
   15.10        (["polynomial","simplification"],
   15.11          [("#Given" ,["Term t_t"]),

    16.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy	Mon Jan 27 13:40:36 2014 +0100
    16.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy	Mon Jan 27 21:49:27 2014 +0100
    16.3 @@ -1014,7 +1014,7 @@
    16.4    PolyEq_prls, SOME "solve (e_e::bool, v_v)",
    16.5    [["PolyEq","complete_square"]]));
    16.6  *}
    16.7 -setup {* KEStore_Elems.store_pbts
    16.8 +setup {* KEStore_Elems.add_pbts
    16.9    [(prep_pbt thy "pbl_equ_univ_poly" [] e_pblID
   16.10        (["polynomial","univariate","equation"],
   16.11          [("#Given" ,["equality e_e","solveFor v_v"]),

    17.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy	Mon Jan 27 13:40:36 2014 +0100
    17.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy	Mon Jan 27 21:49:27 2014 +0100
    17.3 @@ -499,7 +499,7 @@
    17.4    SOME "Probe e_e w_w", 
    17.5    [["probe","fuer_bruch"]]));
    17.6  *}
    17.7 -setup {* KEStore_Elems.store_pbts
    17.8 +setup {* KEStore_Elems.add_pbts
    17.9    [(prep_pbt thy "pbl_vereinf_poly" [] e_pblID
   17.10        (["polynom","vereinfachen"], [], Erls, NONE, [])),
   17.11      (prep_pbt thy "pbl_vereinf_poly_minus" [] e_pblID

    18.1 --- a/src/Tools/isac/Knowledge/RatEq.thy	Mon Jan 27 13:40:36 2014 +0100
    18.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy	Mon Jan 27 21:49:27 2014 +0100
    18.3 @@ -194,7 +194,7 @@
    18.4    RatEq_prls, SOME "solve (e_e::bool, v_v)",
    18.5    [["RatEq","solve_rat_equation"]]));
    18.6  *}
    18.7 -setup {* KEStore_Elems.store_pbts
    18.8 +setup {* KEStore_Elems.add_pbts
    18.9    [(prep_pbt thy "pbl_equ_univ_rat" [] e_pblID
   18.10      (["rational","univariate","equation"],
   18.11        [("#Given", ["equality e_e","solveFor v_v"]),

    19.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Mon Jan 27 13:40:36 2014 +0100
    19.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Mon Jan 27 21:49:27 2014 +0100
    19.3 @@ -896,7 +896,7 @@
    19.4    SOME "Simplify t_t", 
    19.5    [["simplification","of_rationals"]]));
    19.6  *}
    19.7 -setup {* KEStore_Elems.store_pbts
    19.8 +setup {* KEStore_Elems.add_pbts
    19.9    [(prep_pbt thy "pbl_simp_rat" [] e_pblID
   19.10        (["rational","simplification"],
   19.11          [("#Given" ,["Term t_t"]),

    20.1 --- a/src/Tools/isac/Knowledge/RootEq.thy	Mon Jan 27 13:40:36 2014 +0100
    20.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy	Mon Jan 27 21:49:27 2014 +0100
    20.3 @@ -523,7 +523,7 @@
    20.4    RootEq_prls,  SOME "solve (e_e::bool, v_v)",
    20.5    [["RootEq","norm_sq_root_equation"]]));
    20.6  *}
    20.7 -setup {* KEStore_Elems.store_pbts
    20.8 +setup {* KEStore_Elems.add_pbts
    20.9    [(prep_pbt thy "pbl_equ_univ_root" [] e_pblID
   20.10        (["root'","univariate","equation"],
   20.11          [("#Given" ,["equality e_e","solveFor v_v"]),

    21.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy	Mon Jan 27 13:40:36 2014 +0100
    21.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy	Mon Jan 27 21:49:27 2014 +0100
    21.3 @@ -150,7 +150,7 @@
    21.4    RootRatEq_prls, SOME "solve (e_e::bool, v_v)",
    21.5    [["RootRatEq","elim_rootrat_equation"]]));
    21.6  *}
    21.7 -setup {* KEStore_Elems.store_pbts
    21.8 +setup {* KEStore_Elems.add_pbts
    21.9    [(prep_pbt thy "pbl_equ_univ_root_sq_rat" [] e_pblID
   21.10        (["rat","sq","root'","univariate","equation"],
   21.11          [("#Given" ,["equality e_e","solveFor v_v"]),

    22.1 --- a/src/Tools/isac/Knowledge/Simplify.thy	Mon Jan 27 13:40:36 2014 +0100
    22.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy	Mon Jan 27 21:49:27 2014 +0100
    22.3 @@ -48,7 +48,7 @@
    22.4    SOME "Vereinfache t_t", 
    22.5    []));
    22.6  *}
    22.7 -setup {* KEStore_Elems.store_pbts
    22.8 +setup {* KEStore_Elems.add_pbts
    22.9    [(prep_pbt thy "pbl_simp" [] e_pblID
   22.10        (["simplification"],
   22.11          [("#Given" ,["Term t_t"]),

    23.1 --- a/src/Tools/isac/Knowledge/Test.thy	Mon Jan 27 13:40:36 2014 +0100
    23.2 +++ b/src/Tools/isac/Knowledge/Test.thy	Mon Jan 27 21:49:27 2014 +0100
    23.3 @@ -570,7 +570,7 @@
    23.4   ------ 25.8.01*)
    23.5  
    23.6  *}
    23.7 -setup {* KEStore_Elems.store_pbts
    23.8 +setup {* KEStore_Elems.add_pbts
    23.9    [(prep_pbt thy "pbl_test" [] e_pblID (["test"], [], e_rls, NONE, [])),
   23.10      (prep_pbt thy "pbl_test_equ" [] e_pblID
   23.11        (["equation","test"],
   23.12 @@ -831,7 +831,7 @@
   23.13  *)
   23.14  
   23.15  *}
   23.16 -setup {* KEStore_Elems.store_pbts
   23.17 +setup {* KEStore_Elems.add_pbts
   23.18    [(prep_pbt thy "pbl_test_uni_plain2" [] e_pblID
   23.19      (["plain_square","univariate","equation","test"],
   23.20        [("#Given" ,["equality e_e","solveFor v_v"]),
   23.21 @@ -921,7 +921,7 @@
   23.22  *)
   23.23  
   23.24  *}
   23.25 -setup {* KEStore_Elems.store_pbts
   23.26 +setup {* KEStore_Elems.add_pbts
   23.27    [(prep_pbt thy "pbl_test_uni_poly" [] e_pblID
   23.28        (["polynomial","univariate","equation","test"],
   23.29          [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),

    24.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_1.thy	Mon Jan 27 13:40:36 2014 +0100
    24.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_1.thy	Mon Jan 27 21:49:27 2014 +0100
    24.3 @@ -1,19 +1,19 @@
    24.4  theory Thy_1 imports Lucas_Interpreter begin
    24.5  
    24.6  ML {* 
    24.7 -  (* CHECK length (KEStore_Elems.get_rlss @{theory}) = length (! ruleset') 
    24.8 +  (* CHECK length (Test_KEStore_Elems.get_rlss @{theory}) = length (! ruleset') 
    24.9      AT THE BOTTOM OF A THEORY:*)
   24.10 -  length (KEStore_Elems.get_rlss @{theory}) = 0;
   24.11 +  length (Test_KEStore_Elems.get_rlss @{theory}) = 0;
   24.12  (*length (! test_ruleset')                  = 1 (* if you have clicked somewhere below *)*)
   24.13  *}
   24.14 -setup {* KEStore_Elems.add_rlss [("test_list_rls", (Context.theory_name @{theory}, Erls))] *}
   24.15 +setup {* Test_KEStore_Elems.add_rlss [("test_list_rls", (Context.theory_name @{theory}, Erls))] *}
   24.16  ML {* 
   24.17  (*test_ruleset' := overwritelthy @{theory} (! test_ruleset', [("test_list_rls", Erls)])
   24.18    ;
   24.19 -  if length (KEStore_Elems.get_rlss @{theory}) = length (! test_ruleset') then ()
   24.20 -    else error "removal of Unsynchonized.ref: ruleset' <> KEStore_Elems.get_rlss in Thy_1"*)
   24.21 +  if length (Test_KEStore_Elems.get_rlss @{theory}) = length (! test_ruleset') then ()
   24.22 +    else error "removal of Unsynchonized.ref: ruleset' <> Test_KEStore_Elems.get_rlss in Thy_1"*)
   24.23  *}
   24.24  
   24.25 -setup {* KEStore_Elems.add_calcs [("calc", ("Thy_1", e_evalfn))] *}
   24.26 +setup {* Test_KEStore_Elems.add_calcs [("calc", ("Thy_1", e_evalfn))] *}
   24.27  
   24.28  end

    25.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_2.thy	Mon Jan 27 13:40:36 2014 +0100
    25.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_2.thy	Mon Jan 27 21:49:27 2014 +0100
    25.3 @@ -3,7 +3,7 @@
    25.4  ML {* val test_list_rls =
    25.5    append_rls "test_list_rls" e_rls [Thm ("refl", @{thm refl}), Thm ("subst", @{thm subst})] *}
    25.6  
    25.7 -setup {* KEStore_Elems.add_rlss 
    25.8 +setup {* Test_KEStore_Elems.add_rlss 
    25.9    [("test_list_rls", (Context.theory_name @{theory}, (*already added in Thy_1.thy*)
   25.10      test_list_rls))] *}
   25.11  

    26.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_2b.thy	Mon Jan 27 13:40:36 2014 +0100
    26.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_2b.thy	Mon Jan 27 21:49:27 2014 +0100
    26.3 @@ -3,7 +3,7 @@
    26.4  ML {* val test_list_rls =
    26.5    append_rls "test_list_rls" e_rls [Thm ("False_def", @{thm False_def})] *}
    26.6  
    26.7 -setup {* KEStore_Elems.add_rlss [("test_list_rls", (Context.theory_name @{theory},
    26.8 +setup {* Test_KEStore_Elems.add_rlss [("test_list_rls", (Context.theory_name @{theory},
    26.9    test_list_rls))] *}
   26.10  ML {* (*test_ruleset' := overwritelthy @{theory} (! test_ruleset', 
   26.11    [("test_list_rls", test_list_rls)])*)

    27.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_3.thy	Mon Jan 27 13:40:36 2014 +0100
    27.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_3.thy	Mon Jan 27 21:49:27 2014 +0100
    27.3 @@ -3,27 +3,27 @@
    27.4  ML {* val test_list_rls =
    27.5    append_rls "test_list_rls" e_rls [Thm ("not_def", @{thm not_def})] *}
    27.6  
    27.7 -setup {* KEStore_Elems.add_rlss (*already added in Thy_1.thy and Thy_2.thy*)
    27.8 +setup {* Test_KEStore_Elems.add_rlss (*already added in Thy_1.thy and Thy_2.thy*)
    27.9    [("test_list_rls", (Context.theory_name @{theory}, test_list_rls))] *}
   27.10  
   27.11  ML {*
   27.12 -  if length (KEStore_Elems.get_rlss @{theory}) = 1 (*stored in 3 different theories*)
   27.13 +  if length (Test_KEStore_Elems.get_rlss @{theory}) = 1 (*stored in 3 different theories*)
   27.14    then () else error "rls identified by string-identifier, not by theory: changed"
   27.15  
   27.16  (*test_ruleset' := overwritelthy @{theory} (! test_ruleset', [("test_list_rls", 
   27.17      append_rls "test_list_rls" test_list_rls [Calc ("test_function", e_evalfn)])])*)
   27.18    ;
   27.19 -(*if length (KEStore_Elems.get_rlss @{theory}) = length (! test_ruleset')
   27.20 -  then () else error "KEStore_Elems.get_rlss = test_ruleset': changed"*)
   27.21 +(*if length (Test_KEStore_Elems.get_rlss @{theory}) = length (! test_ruleset')
   27.22 +  then () else error "Test_KEStore_Elems.get_rlss = test_ruleset': changed"*)
   27.23    ;
   27.24    val SOME (_, Rls {rules, ...}) =
   27.25 -    AList.lookup op= (KEStore_Elems.get_rlss @{theory}) "test_list_rls"
   27.26 +    AList.lookup op= (Test_KEStore_Elems.get_rlss @{theory}) "test_list_rls"
   27.27    ;
   27.28    case rules of
   27.29      [Thm ("not_def", _)] => ()
   27.30    | _ => error "union rls_eq changed: 1st argument is NOT overwritten anymore"
   27.31    (* merge rules of rls with the same identifier rls' must be done one level higher:
   27.32 -    KEStore_Elems.add_rlss does *add* or *overwrite* *)
   27.33 +    Test_KEStore_Elems.add_rlss does *add* or *overwrite* *)
   27.34  *}
   27.35  
   27.36  end

    28.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_4.thy	Mon Jan 27 13:40:36 2014 +0100
    28.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_4.thy	Mon Jan 27 21:49:27 2014 +0100
    28.3 @@ -1,5 +1,5 @@
    28.4  theory Thy_4 imports Lucas_Interpreter (*!!!!!*) begin
    28.5  
    28.6 -setup {* KEStore_Elems.add_rlss [("rls1", ("Thy_4", Erls)), ("rls2", ("Thy_4", Erls))] *}
    28.7 +setup {* Test_KEStore_Elems.add_rlss [("rls1", ("Thy_4", Erls)), ("rls2", ("Thy_4", Erls))] *}
    28.8  
    28.9  end

    29.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_5.thy	Mon Jan 27 13:40:36 2014 +0100
    29.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_5.thy	Mon Jan 27 21:49:27 2014 +0100
    29.3 @@ -1,5 +1,5 @@
    29.4  theory Thy_5 imports Thy_4 begin
    29.5  
    29.6 -setup {* KEStore_Elems.add_rlss [("rls", ("Thy_5", Erls))] *}
    29.7 +setup {* Test_KEStore_Elems.add_rlss [("rls", ("Thy_5", Erls))] *}
    29.8  
    29.9  end                             

    30.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_All.thy	Mon Jan 27 13:40:36 2014 +0100
    30.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_All.thy	Mon Jan 27 21:49:27 2014 +0100
    30.3 @@ -1,7 +1,7 @@
    30.4  theory Thy_All imports Thy_3 Thy_5 begin
    30.5  
    30.6  ML {*
    30.7 -KEStore_Elems.get_rlss @{theory}
    30.8 +Test_KEStore_Elems.get_rlss @{theory}
    30.9  (*|> map check_kestore_rls 
   30.10    |> enumerate_strings
   30.11    |> map writeln*)
   30.12 @@ -12,13 +12,13 @@
   30.13  (test_list_rls, (Thy_3, Rls {#calc = 0, #rules = 1, ...))--4 
   30.14  *)
   30.15  ;
   30.16 -case KEStore_Elems.get_rlss @{theory} of
   30.17 +case Test_KEStore_Elems.get_rlss @{theory} of
   30.18    ("rls2", ("Thy_4", Erls)) :: ("rls1", ("Thy_4", Erls)) :: _ => ()
   30.19 -| _ => raise error "KEStore_Elems.get_rlss changed"
   30.20 +| _ => raise error "Test_KEStore_Elems.get_rlss changed"
   30.21  ;
   30.22 -case KEStore_Elems.get_calcs @{theory} of
   30.23 +case Test_KEStore_Elems.get_calcs @{theory} of
   30.24    [("calc", ("Thy_1", _))] => ()
   30.25 -| _ => raise error "KEStore_Elems.get_calcs changed"
   30.26 +| _ => raise error "Test_KEStore_Elems.get_calcs changed"
   30.27  *}
   30.28  
   30.29  end

    31.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml	Mon Jan 27 13:40:36 2014 +0100
    31.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml	Mon Jan 27 21:49:27 2014 +0100
    31.3 @@ -14,7 +14,7 @@
    31.4    (*etc*)
    31.5  end;                               
    31.6  
    31.7 -structure KEStore_Elems: KESTORE_ELEMS =
    31.8 +structure Test_KEStore_Elems: KESTORE_ELEMS =
    31.9  struct
   31.10    fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
   31.11  

    32.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Mon Jan 27 13:40:36 2014 +0100
    32.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Mon Jan 27 21:49:27 2014 +0100
    32.3 @@ -892,7 +892,7 @@
    32.4     (prep_pbt thy "pbl_SP_Ztrans" [] e_pblID
    32.5     (["Z_Transform","SignalProcessing"], [], e_rls, NONE, []));
    32.6  *}
    32.7 -setup {* store_pbts
    32.8 +setup {* KEStore_Elems.add_pbts
    32.9    [prep_pbt thy "pbl_SP" [] e_pblID (["SignalProcessing"], [], e_rls, NONE, []),
   32.10      prep_pbt thy "pbl_SP_Ztrans" [] e_pblID
   32.11        (["Z_Transform","SignalProcessing"], [], e_rls, NONE, [])] *}
   32.12 @@ -911,7 +911,7 @@
   32.13      append_rls "e_rls" e_rls [(*for preds in where_*)], NONE, 
   32.14      [["SignalProcessing","Z_Transform","Inverse"]]));
   32.15  *}
   32.16 -setup {* store_pbts
   32.17 +setup {* KEStore_Elems.add_pbts
   32.18    [prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID
   32.19        (["Inverse", "Z_Transform", "SignalProcessing"],
   32.20          [("#Given", ["filterExpression X_eq"]),

    33.1 --- a/test/Tools/isac/Interpret/rewtools.sml	Mon Jan 27 13:40:36 2014 +0100
    33.2 +++ b/test/Tools/isac/Interpret/rewtools.sml	Mon Jan 27 21:49:27 2014 +0100
    33.3 @@ -73,12 +73,12 @@
    33.4  val isabthms = (flat o (map Theory.axioms_of)) ancestors;
    33.5  
    33.6  val isacrules = (flat o (map (thms_of_rls o #2 o #2))) 
    33.7 -  (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"));
    33.8 +  (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"));
    33.9  (*thms from rulesets*)
   33.10  (*=== inhibit exn AK110725 =============================================================
   33.11  val isacrlsthms = ((map rep_thm_G') o flat o 
   33.12  		 (map (PureThy.all_thms_of_rls o #2 o #2))) 
   33.13 -		   (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"));
   33.14 +		   (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"));
   33.15  length isacrlsthms;
   33.16  (*takes a few seconds...
   33.17  val isacrlsthms = gen_distinct eq_thmI isacrlsthms;
   33.18 @@ -159,14 +159,14 @@
   33.19  curry ((op mem) o swap) dropthys' "Isac";
   33.20  		val ancestors_rls = 
   33.21  		  filter_out ((curry ((op mem) o swap) dropthys') o ((#1 o #2): rls'*(theory' * rls)->theory'))
   33.22 -		     (rev (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")));
   33.23 +		     (rev (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")));
   33.24  
   33.25  take (10, map #1 ancestors_rls) = 
   33.26    ["expand_binomtest", "make_polytest", "rearrange_assoc", "ac_plus_times", "norm_equation", 
   33.27     "matches", "isolate_bdv", "isolate_root", "tval_rls", "Test_simplify"]; (*..all rls in each*)
   33.28  
   33.29  (* WN120523 popped up again ?!?!?
   33.30 -if length (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")) <> length ancestors_rls then ()
   33.31 +if length (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")) <> length ancestors_rls then ()
   33.32  else error "rewtools.sml: diff.behav. in thy_containing_rls 2 ERRATICAL?";
   33.33  *)
   33.34  
   33.35 @@ -191,7 +191,7 @@
   33.36      val dropthys' = map (get_thy o (#1 : (theory' * theory) -> theory')) dropthys: string list;
   33.37  		    val ancestors_rls = 
   33.38  		      filter_out ((curry ((op mem) o swap) dropthys') o ((#1 o #2): rls'*(theory' * rls)->theory'))
   33.39 -		        (rev (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")));
   33.40 +		        (rev (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")));
   33.41  		
   33.42  case assoc (ancestors_rls, rls') of
   33.43    SOME ("Poly", Seq {id = "norm_Poly", ...}) => ()
   33.44 @@ -218,13 +218,13 @@
   33.45    "LinEq", "Root", "Equation", "Rational", "Poly", "Simplify"] (*, "Atools", ..*)
   33.46  then () else error "thy_containing_cal changed ancestors_rls for Atools";
   33.47  
   33.48 -Thy_Info.get_theory thy' |> KEStore_Elems.get_calcs |> rev;
   33.49 -Thy_Info.get_theory thy' |> KEStore_Elems.get_calcs |> rev |> map #1;
   33.50 -Thy_Info.get_theory thy' |> KEStore_Elems.get_calcs |> rev |> map (#1 : calc -> string);
   33.51 +Thy_Info.get_theory thy' |> Test_KEStore_Elems.get_calcs |> rev;
   33.52 +Thy_Info.get_theory thy' |> Test_KEStore_Elems.get_calcs |> rev |> map #1;
   33.53 +Thy_Info.get_theory thy' |> Test_KEStore_Elems.get_calcs |> rev |> map (#1 : calc -> string);
   33.54  
   33.55      val ancestors_cal =
   33.56        filter_out ((curry ((op mem) o swap) dropthys') o (#1 : calc -> string))
   33.57 -        (Thy_Info.get_theory thy' |> KEStore_Elems.get_calcs |> rev);
   33.58 +        (Thy_Info.get_theory thy' |> Test_KEStore_Elems.get_calcs |> rev);
   33.59  
   33.60  if thy_containing_cal "Biegelinie" "PLUS" = ("IsacKnowledge", "plus") 
   33.61                      (*WN120410: SHOULD BE = ("IsacKnowledge", "Atools")*)

    34.1 --- a/test/Tools/isac/Knowledge/build_thydata.sml	Mon Jan 27 13:40:36 2014 +0100
    34.2 +++ b/test/Tools/isac/Knowledge/build_thydata.sml	Mon Jan 27 21:49:27 2014 +0100
    34.3 @@ -30,14 +30,14 @@
    34.4  
    34.5  local
    34.6      val isacrlsthms = ((gen_distinct eq_thmI) o (map rep_thm_G') o flat o 
    34.7 -		       (map (thms_of_rls o #2 o #2))) (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"));
    34.8 +		       (map (thms_of_rls o #2 o #2))) (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"));
    34.9      val isacthms = (flat o (map (thms_of o #2))) (!theory');
   34.10  in
   34.11      val rlsthmsNOTisac = gen_diff eq_thmI (isacrlsthms, isacthms);
   34.12  end;
   34.13  *)
   34.14      val isacrlsthms''''' = ((gen_distinct eq_thmI) o (map rep_thm_G') o flat o 
   34.15 -		       (map (thms_of_rls o #2 o #2))) (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"))
   34.16 +		       (map (thms_of_rls o #2 o #2))) (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"))
   34.17  		         :  (thmID * thm) list;
   34.18  (* THIS IS TOO EXPENSIVE:
   34.19  val all_ListC_thms = Global_Theory.all_thms_of (@{theory "ListC"});
   34.20 @@ -137,7 +137,7 @@
   34.21  "-------- prop_of thm .. Theory.axioms_of ---------------";
   34.22  "-------- prop_of thm .. Theory.axioms_of ---------------";
   34.23  "-------- prop_of thm .. Theory.axioms_of ---------------";
   34.24 -val isacrlsthms''''' = (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"))
   34.25 +val isacrlsthms''''' = (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"))
   34.26    |> map (thms_of_rls o #2 o #2) (*drop manually input id in Thm (id, thm)*)
   34.27    |> flat
   34.28    |> map thm_of_thm
   34.29 @@ -247,7 +247,7 @@
   34.30  "----- so we cannot get isacthms as thm, only as term ---";
   34.31  "----- but we can retain isacrlsthms as thm ---";
   34.32  *)
   34.33 -val isacrlsthms = (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"))
   34.34 +val isacrlsthms = (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"))
   34.35    |> map (thms_of_rls o #2 o #2) (*drop manually input id in Thm (id, thm)*)
   34.36    |> flat
   34.37    |> map thm_of_thm

    35.1 --- a/test/Tools/isac/OLDTESTS/script_if.sml	Mon Jan 27 13:40:36 2014 +0100
    35.2 +++ b/test/Tools/isac/OLDTESTS/script_if.sml	Mon Jan 27 21:49:27 2014 +0100
    35.3 @@ -65,7 +65,7 @@
    35.4  			  eval_is_rootequation_in "")],
    35.5    [("Test","methode")]));
    35.6  
    35.7 -store_pbts
    35.8 +Test_KEStore_Elems.add_pbts
    35.9    [prep_pbt (*Test.thy*) (theory "Isac")
   35.10        (["root'","univariate","equation","test"],
   35.11          [("#Given" ,["equality e_e","solveFor v_v"]),
   35.12 @@ -90,7 +90,7 @@
   35.13    append_rls e_rls [Calc ("Tools.matches",eval_matches "#matches_")],
   35.14    []));
   35.15  
   35.16 -store_pbts
   35.17 +Test_KEStore_Elems.add_pbts
   35.18    [prep_pbt (theory "Isac")
   35.19        (["approximate","univariate","equation","test"],
   35.20          [("#Given", ["equality e_e","solveFor v_v","errorBound err_"]),

    36.1 --- a/test/Tools/isac/OLDTESTS/scriptnew.sml	Mon Jan 27 13:40:36 2014 +0100
    36.2 +++ b/test/Tools/isac/OLDTESTS/scriptnew.sml	Mon Jan 27 21:49:27 2014 +0100
    36.3 @@ -32,7 +32,7 @@
    36.4    ],
    36.5    e_rls, NONE, []));
    36.6  
    36.7 -store_pbts
    36.8 +Test_KEStore_Elems.add_pbts
    36.9    [prep_pbt Test.thy "pbl_testss" [] e_pblID
   36.10        (["tests"], []:(string * string list) list, e_rls, NONE, []),
   36.11      prep_pbt Test.thy "pbl_testss_term" [] e_pblID
   36.12 @@ -109,7 +109,7 @@
   36.13     ("#Find"  ,["boolTestFind v_i_"])
   36.14    ],
   36.15    e_rls, NONE, []));
   36.16 -store_pbts
   36.17 +Test_KEStore_Elems.add_pbts
   36.18    [prep_pbt Test.thy "pbl_testss_eq" [] e_pblID
   36.19        (["met_testeq","tests"],
   36.20          [("#Given" ,["boolTestGiven e_e"]),

    37.1 --- a/test/Tools/isac/Test_Isac.thy	Mon Jan 27 13:40:36 2014 +0100
    37.2 +++ b/test/Tools/isac/Test_Isac.thy	Mon Jan 27 21:49:27 2014 +0100
    37.3 @@ -45,20 +45,39 @@
    37.4    ML {*"%%%%%%%%%%%%%%%%% end Isabelle %%%%%%%%%%%%%%%%%%%%%%%%%";*}
    37.5  
    37.6  section {* test ML Code of isac *}
    37.7 +  setup {* KEStore_Elems.add_pbts
    37.8 +    [prep_pbt @{theory "Test"} "pbl_ttest" [] e_pblID (["test"], [], e_rls, NONE, []),
    37.9 +      prep_pbt @{theory "Test"} "pbl_ttest_calc" [] e_pblID
   37.10 +        (["calculate","test"],
   37.11 +          [("#Given" ,["realTestGiven t_t"]),
   37.12 +            ("#Find"  ,["realTestFind s_s"])],
   37.13 +          e_rls, NONE, [["Test","test_calculate"]]),
   37.14 +       prep_pbt thy "pbl_test_refine" [] e_pblID (["refine", "test"], [], e_rls, NONE, []),
   37.15 +       prep_pbt @{theory DiffApp} "pbl_pbla" [] e_pblID
   37.16 +         (["pbla", "refine", "test"], [("#Given", ["fixedValues a_a"])], e_rls, NONE, []),
   37.17 +       prep_pbt @{theory DiffApp} "pbl_pbla1" [] e_pblID
   37.18 +         (["pbla1","pbla", "refine", "test"],
   37.19 +           [("#Given", ["fixedValues a_a","maximum a_1"])], e_rls, NONE, []),
   37.20 +       prep_pbt @{theory DiffApp} "pbl_pbla2" [] e_pblID
   37.21 +         (["pbla2","pbla", "refine", "test"], 
   37.22 +           [("#Given", ["fixedValues a_a","valuesFor a_2"])], e_rls, NONE, []),
   37.23 +       prep_pbt @{theory DiffApp} "pbl_pbla2x" [] e_pblID
   37.24 +         (["pbla2x","pbla2","pbla", "refine", "test"],
   37.25 +           [("#Given", ["fixedValues a_a","valuesFor a_2","functionOf a2_x"])], e_rls, NONE, []),
   37.26 +       prep_pbt @{theory DiffApp} "pbl_pbla2y" [] e_pblID
   37.27 +         (["pbla2y","pbla2","pbla", "refine", "test"],
   37.28 +           [("#Given" ,["fixedValues a_a","valuesFor a_2","boundVariable a2_y"])], e_rls, NONE, []),
   37.29 +       prep_pbt @{theory DiffApp} "pbl_pbla2z" [] e_pblID
   37.30 +         (["pbla2z","pbla2","pbla", "refine", "test"],
   37.31 +           [("#Given" ,["fixedValues a_a","valuesFor a_2","interval a2_z"])], e_rls, NONE, []),
   37.32 +       prep_pbt @{theory DiffApp} "pbl_pbla3" [] e_pblID
   37.33 +         (["pbla3","pbla", "refine", "test"],
   37.34 +           [("#Given" ,["fixedValues a_a","relations a_3"])], e_rls, NONE, [])] *}
   37.35    ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*}
   37.36    ML_file          "library.sml"
   37.37    ML_file          "calcelems.sml"
   37.38    ML_file          "kestore.sml"
   37.39    ML_file "ProgLang/termC.sml"
   37.40 -
   37.41 -  setup {* store_pbts
   37.42 -    [prep_pbt @{theory "Test"} "pbl_ttest" [] e_pblID (["test"], [], e_rls, NONE, []),
   37.43 -      prep_pbt @{theory "Test"} "pbl_ttest_calc" [] e_pblID
   37.44 -        (["calculate","test"],
   37.45 -          [("#Given" ,["realTestGiven t_t"]),
   37.46 -            ("#Find"  ,["realTestFind s_s"])],
   37.47 -          e_rls, NONE, [["Test","test_calculate"]])] *}
   37.48 -
   37.49    ML_file "ProgLang/calculate.sml"
   37.50    ML_file "ProgLang/rewrite.sml"
   37.51    ML_file "ProgLang/listC.sml"

    38.1 --- a/test/Tools/isac/kestore.sml	Mon Jan 27 13:40:36 2014 +0100
    38.2 +++ b/test/Tools/isac/kestore.sml	Mon Jan 27 21:49:27 2014 +0100
    38.3 @@ -8,7 +8,7 @@
    38.4  "table of contents -----------------------------------------------------------";
    38.5  "-----------------------------------------------------------------------------";
    38.6  "-------- fun check_kestore_rls ----------------------------------------------";
    38.7 -"-------- fun KEStore_Elems.add_rlss overwrites earlier data -----------------";
    38.8 +"-------- fun Test_KEStore_Elems.add_rlss overwrites earlier data ------------";
    38.9  "-----------------------------------------------------------------------------";
   38.10  "-----------------------------------------------------------------------------";
   38.11  
   38.12 @@ -19,16 +19,16 @@
   38.13    "(e_rls, (KEStore, Rls {#calc = 0, #rules = 0, ...))"
   38.14  then () else error "check_kestore_rls changed"
   38.15  ;
   38.16 -KEStore_Elems.get_rlss @{theory Isac} 
   38.17 +Test_KEStore_Elems.get_rlss @{theory Isac} 
   38.18    |> map check_kestore_rls 
   38.19    |> enumerate_strings
   38.20    |> sort string_ord
   38.21  (*|> map writeln*)
   38.22  ;
   38.23  
   38.24 -"-------- fun KEStore_Elems.add_rlss overwrites earlier data -----------------";
   38.25 -"-------- fun KEStore_Elems.add_rlss overwrites earlier data -----------------";
   38.26 -"-------- fun KEStore_Elems.add_rlss overwrites earlier data -----------------";
   38.27 +"-------- fun Test_KEStore_Elems.add_rlss overwrites earlier data -----------------";
   38.28 +"-------- fun Test_KEStore_Elems.add_rlss overwrites earlier data -----------------";
   38.29 +"-------- fun Test_KEStore_Elems.add_rlss overwrites earlier data -----------------";
   38.30    fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
   38.31    fun rls_eq ((id1, (thyID1, _)), (id2, (thyID2, _))) = id1 = id2 (*andalso thyID1 = thyID2*)
   38.32  

    39.1 --- a/test/Tools/isac/xmlsrc/thy-hierarchy.sml	Mon Jan 27 13:40:36 2014 +0100
    39.2 +++ b/test/Tools/isac/xmlsrc/thy-hierarchy.sml	Mon Jan 27 21:49:27 2014 +0100
    39.3 @@ -38,7 +38,7 @@
    39.4  overwrite (al, b);
    39.5  overwritelthy thy (al, bl);
    39.6  
    39.7 -case assoc' ((KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")),"e_rls") of
    39.8 +case assoc' ((Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")),"e_rls") of
    39.9    SOME ("Tools", Rls _) => ()
   39.10  | _ => error "e_rls not in Theory_Data" 
   39.11  
   39.12 @@ -80,7 +80,7 @@
   39.13  val thy' = "Test";
   39.14  val rlss = filter ((curry op= thy') o 
   39.15  			   ((#1 o #2):(rls' * (theory' * rls)) -> theory')) 
   39.16 -			  (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"));
   39.17 +			  (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"));
   39.18  collect_rlss ("IsacKnowledge",thy');
   39.19  
   39.20  "collect_thy thy-------------------------------------------------";
   39.21 @@ -388,7 +388,7 @@
   39.22      val dropthys' = map (get_thy o (#1 : (theory' * theory) -> theory')) dropthys: string list;
   39.23  		    val ancestors_rls = 
   39.24  		      filter_out ((curry ((op mem) o swap) dropthys') o ((#1 o #2): rls'*(theory' * rls)->theory'))
   39.25 -		        (rev (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")));
   39.26 +		        (rev (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")));
   39.27  
   39.28  case assoc (ancestors_rls, rls') of
   39.29    SOME ("Poly", Rls {id = "discard_minus", ...}) => ()