# HG changeset patch
# User Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at>
# Date 1390855767 -3600
# Node ID 73dc85c025abb9d01b4ffe46018f3f068827abaa
# Parent  b1f0389ca11f8d419fb90313d50a88697fde86eb
cleanup, naming: 'KEStore_Elems' in Tests now 'Test_KEStore_Elems', 'store_pbts' now 'add_pbts'

diff -r b1f0389ca11f -r 73dc85c025ab src/Tools/isac/KEStore.thy
--- a/src/Tools/isac/KEStore.thy	Mon Jan 27 13:40:36 2014 +0100
+++ b/src/Tools/isac/KEStore.thy	Mon Jan 27 21:49:27 2014 +0100
@@ -26,8 +26,7 @@
   val get_cas: theory -> cas_elem list
   val add_cas: cas_elem list -> theory -> theory
   val get_ptyps: theory -> ptyps
-  val store_pbts: (pbt * pblID) list -> theory -> theory
-  val add_pbt: (pbt * pblID) -> theory -> theory
+  val add_pbts: (pbt * pblID) list -> theory -> theory
   (*etc*)
 end;                               
 
@@ -69,13 +68,12 @@
     val merge = merge_ptyps;
     );
   fun get_ptyps thy = Data.get thy;
-  fun store_pbts pbts = let
-          fun store_pbts' (pbt, pblID) = rev pblID |> insrt pblID pbt;
-        in fold store_pbts' pbts |> Data.map end;
-  (* the pblID has the leaf-element as first; better readability achieved *)
-  fun add_pbt (pbt as {guh,...}, pblID) = 
-    (if (!check_guhs_unique) then check_pblguh_unique guh (! ptyps) else ();
-    Data.map (insrt pblID pbt (rev pblID)))
+  fun add_pbts pbts thy = let
+          fun add_pbt (pbt as {guh,...}, pblID) =
+                (* the pblID has the leaf-element as first; better readability achieved *)
+                (if (!check_guhs_unique) then check_pblguh_unique guh (Data.get thy) else ();
+                  rev pblID |> insrt pblID pbt);
+        in Data.map (fold add_pbt pbts) thy end;
 
   (*etc*)
 end;
@@ -116,10 +114,9 @@
 
 fun assoc_cas thy key = assoc (KEStore_Elems.get_cas thy, key);
 
-fun get_ptyps () = ! ptyps 
+fun get_ptyps () = ! ptyps;
 (*SWITCH:
-fun get_ptyps () = Thy_Info.get_theory "Build_Knowledge" |> KEStore_Elems.get_ptyps*);
-val store_pbts = KEStore_Elems.store_pbts;
+fun get_ptyps () = Thy_Info.get_theory "Build_Knowledge" |> KEStore_Elems.get_ptyps*)
 
 (*SWITCH: outcomment store_pbt, if all occurrences in src+test have in parallel 
   SETUP ..* KEStore_Elems.add_pbt (.....) *.. 
diff -r b1f0389ca11f -r 73dc85c025ab src/Tools/isac/Knowledge/AlgEin.thy
--- a/src/Tools/isac/Knowledge/AlgEin.thy	Mon Jan 27 13:40:36 2014 +0100
+++ b/src/Tools/isac/Knowledge/AlgEin.thy	Mon Jan 27 21:49:27 2014 +0100
@@ -55,7 +55,7 @@
 (* show_ptyps();
    *)
 *}
-setup {* KEStore_Elems.store_pbts
+setup {* KEStore_Elems.add_pbts
   [(prep_pbt thy "pbl_algein" [] e_pblID (["Berechnung"], [], e_rls, NONE, [])),
     (prep_pbt thy "pbl_algein_numsym" [] e_pblID
       (["numerischSymbolische", "Berechnung"],
diff -r b1f0389ca11f -r 73dc85c025ab src/Tools/isac/Knowledge/Biegelinie.thy
--- a/src/Tools/isac/Knowledge/Biegelinie.thy	Mon Jan 27 13:40:36 2014 +0100
+++ b/src/Tools/isac/Knowledge/Biegelinie.thy	Mon Jan 27 21:49:27 2014 +0100
@@ -175,7 +175,7 @@
   [["Equation","fromFunction"]]));
 KEStore_Elems.get_ptyps @{theory};
 *}
-setup {* KEStore_Elems.store_pbts
+setup {* KEStore_Elems.add_pbts
   [(prep_pbt thy "pbl_bieg" [] e_pblID
       (["Biegelinien"],
         [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q"]),
diff -r b1f0389ca11f -r 73dc85c025ab src/Tools/isac/Knowledge/Diff.thy
--- a/src/Tools/isac/Knowledge/Diff.thy	Mon Jan 27 13:40:36 2014 +0100
+++ b/src/Tools/isac/Knowledge/Diff.thy	Mon Jan 27 21:49:27 2014 +0100
@@ -272,7 +272,7 @@
   append_rls "e_rls" e_rls [],
   SOME "Differentiate (f_f, v_v)", [["diff","differentiate_equality"]]));
 *}
-setup {* KEStore_Elems.store_pbts
+setup {* KEStore_Elems.add_pbts
   [(prep_pbt thy "pbl_fun" [] e_pblID (["function"], [], e_rls, NONE, [])),
     (prep_pbt thy "pbl_fun_deriv" [] e_pblID
       (["derivative_of","function"],
diff -r b1f0389ca11f -r 73dc85c025ab src/Tools/isac/Knowledge/DiffApp.thy
--- a/src/Tools/isac/Knowledge/DiffApp.thy	Mon Jan 27 13:40:36 2014 +0100
+++ b/src/Tools/isac/Knowledge/DiffApp.thy	Mon Jan 27 21:49:27 2014 +0100
@@ -136,7 +136,7 @@
   ],
   e_rls, NONE, []));
 *}
-setup {* KEStore_Elems.store_pbts
+setup {* KEStore_Elems.add_pbts
   [(prep_pbt thy "pbl_fun_max" [] e_pblID
       (["maximum_of","function"],
         [("#Given" ,["fixedValues f_ix"]),
diff -r b1f0389ca11f -r 73dc85c025ab src/Tools/isac/Knowledge/DiophantEq.thy
--- a/src/Tools/isac/Knowledge/DiophantEq.thy	Mon Jan 27 13:40:36 2014 +0100
+++ b/src/Tools/isac/Knowledge/DiophantEq.thy	Mon Jan 27 21:49:27 2014 +0100
@@ -31,7 +31,7 @@
   e_rls, SOME "solve (e_e::bool, v_v::int)",
   [["LinEq","solve_lineq_equation"]])); (*-----TODO*)
 *}
-setup {* KEStore_Elems.store_pbts
+setup {* KEStore_Elems.add_pbts
   [(prep_pbt thy "pbl_equ_dio" [] e_pblID
       (["diophantine","equation"],
         [("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),
diff -r b1f0389ca11f -r 73dc85c025ab src/Tools/isac/Knowledge/EqSystem.thy
--- a/src/Tools/isac/Knowledge/EqSystem.thy	Mon Jan 27 13:40:36 2014 +0100
+++ b/src/Tools/isac/Knowledge/EqSystem.thy	Mon Jan 27 21:49:27 2014 +0100
@@ -539,7 +539,7 @@
    *)
 
 *}
-setup {* KEStore_Elems.store_pbts
+setup {* KEStore_Elems.add_pbts
   [(prep_pbt thy "pbl_equsys" [] e_pblID
       (["system"],
         [("#Given" ,["equalities e_s", "solveForVars v_s"]),
diff -r b1f0389ca11f -r 73dc85c025ab src/Tools/isac/Knowledge/Equation.thy
--- a/src/Tools/isac/Knowledge/Equation.thy	Mon Jan 27 13:40:36 2014 +0100
+++ b/src/Tools/isac/Knowledge/Equation.thy	Mon Jan 27 21:49:27 2014 +0100
@@ -69,7 +69,7 @@
   ],
   univariate_equation_prls,SOME "solve (e_e::bool, v_v)",[]));
 *}
-setup {* KEStore_Elems.store_pbts
+setup {* KEStore_Elems.add_pbts
   [(prep_pbt thy "pbl_equ" [] e_pblID
       (["equation"],
         [("#Given" ,["equality e_e","solveFor v_v"]),
diff -r b1f0389ca11f -r 73dc85c025ab src/Tools/isac/Knowledge/InsSort.thy
--- a/src/Tools/isac/Knowledge/InsSort.thy	Mon Jan 27 13:40:36 2014 +0100
+++ b/src/Tools/isac/Knowledge/InsSort.thy	Mon Jan 27 21:49:27 2014 +0100
@@ -77,7 +77,7 @@
   ],
   []));
 *}
-setup {* KEStore_Elems.store_pbts
+setup {* KEStore_Elems.add_pbts
   [(prep_pbt @{theory "InsSort"}
       (["functional"]:pblID,
         [("#Given" ,["unsorted u_"]), ("#Find"  ,["sorted s_"])], [])),
diff -r b1f0389ca11f -r 73dc85c025ab src/Tools/isac/Knowledge/Integrate.thy
--- a/src/Tools/isac/Knowledge/Integrate.thy	Mon Jan 27 13:40:36 2014 +0100
+++ b/src/Tools/isac/Knowledge/Integrate.thy	Mon Jan 27 21:49:27 2014 +0100
@@ -359,7 +359,7 @@
   [["diff","integration","named"]]));
  
 *}
-setup {* KEStore_Elems.store_pbts
+setup {* KEStore_Elems.add_pbts
   [(prep_pbt thy "pbl_fun_integ" [] e_pblID
       (["integrate","function"],
         [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
diff -r b1f0389ca11f -r 73dc85c025ab src/Tools/isac/Knowledge/Inverse_Z_Transform.thy
--- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Mon Jan 27 13:40:36 2014 +0100
+++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Mon Jan 27 21:49:27 2014 +0100
@@ -73,7 +73,7 @@
     append_rls "e_rls" e_rls [(*for preds in where_*)], NONE, 
     [["SignalProcessing","Z_Transform","Inverse"]]));
 *}
-setup {* KEStore_Elems.store_pbts
+setup {* KEStore_Elems.add_pbts
   [(prep_pbt thy "pbl_SP" [] e_pblID (["SignalProcessing"], [], e_rls, NONE, [])),
     (prep_pbt thy "pbl_SP_Ztrans" [] e_pblID
       (["Z_Transform","SignalProcessing"], [], e_rls, NONE, [])),
diff -r b1f0389ca11f -r 73dc85c025ab src/Tools/isac/Knowledge/LinEq.thy
--- a/src/Tools/isac/Knowledge/LinEq.thy	Mon Jan 27 13:40:36 2014 +0100
+++ b/src/Tools/isac/Knowledge/LinEq.thy	Mon Jan 27 21:49:27 2014 +0100
@@ -140,7 +140,7 @@
   LinEq_prls, SOME "solve (e_e::bool, v_v)",
   [["LinEq","solve_lineq_equation"]]));
 *}
-setup {* KEStore_Elems.store_pbts
+setup {* KEStore_Elems.add_pbts
   [(prep_pbt thy "pbl_equ_univ_lin" [] e_pblID
       (["LINEAR", "univariate", "equation"],
         [("#Given" ,["equality e_e", "solveFor v_v"]),
diff -r b1f0389ca11f -r 73dc85c025ab src/Tools/isac/Knowledge/LogExp.thy
--- a/src/Tools/isac/Knowledge/LogExp.thy	Mon Jan 27 13:40:36 2014 +0100
+++ b/src/Tools/isac/Knowledge/LogExp.thy	Mon Jan 27 21:49:27 2014 +0100
@@ -40,7 +40,7 @@
   PolyEq_prls, SOME "solve (e_e::bool, v_v)",
   [["Equation","solve_log"]]));
 *}
-setup {* KEStore_Elems.store_pbts
+setup {* KEStore_Elems.add_pbts
   [(prep_pbt thy "pbl_test_equ_univ_log" [] e_pblID
       (["logarithmic","univariate","equation"],
         [("#Given",["equality e_e","solveFor v_v"]),
diff -r b1f0389ca11f -r 73dc85c025ab src/Tools/isac/Knowledge/Partial_Fractions.thy
--- a/src/Tools/isac/Knowledge/Partial_Fractions.thy	Mon Jan 27 13:40:36 2014 +0100
+++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy	Mon Jan 27 21:49:27 2014 +0100
@@ -182,7 +182,7 @@
   NONE, 
   [["simplification","of_rationals","to_partial_fraction"]]));
 *}
-setup {* KEStore_Elems.store_pbts
+setup {* KEStore_Elems.add_pbts
   [(prep_pbt @{theory} "pbl_simp_rat_partfrac" [] e_pblID
       (["partial_fraction", "rational", "simplification"],
         [("#Given" ,["functionTerm t_t", "solveFor v_v"]),
diff -r b1f0389ca11f -r 73dc85c025ab src/Tools/isac/Knowledge/Poly.thy
--- a/src/Tools/isac/Knowledge/Poly.thy	Mon Jan 27 13:40:36 2014 +0100
+++ b/src/Tools/isac/Knowledge/Poly.thy	Mon Jan 27 21:49:27 2014 +0100
@@ -1607,7 +1607,7 @@
   SOME "Simplify t_t", 
   [["simplification","for_polynomials"]]));
 *}
-setup {* KEStore_Elems.store_pbts
+setup {* KEStore_Elems.add_pbts
   [(prep_pbt thy "pbl_simp_poly" [] e_pblID
       (["polynomial","simplification"],
         [("#Given" ,["Term t_t"]),
diff -r b1f0389ca11f -r 73dc85c025ab src/Tools/isac/Knowledge/PolyEq.thy
--- a/src/Tools/isac/Knowledge/PolyEq.thy	Mon Jan 27 13:40:36 2014 +0100
+++ b/src/Tools/isac/Knowledge/PolyEq.thy	Mon Jan 27 21:49:27 2014 +0100
@@ -1014,7 +1014,7 @@
   PolyEq_prls, SOME "solve (e_e::bool, v_v)",
   [["PolyEq","complete_square"]]));
 *}
-setup {* KEStore_Elems.store_pbts
+setup {* KEStore_Elems.add_pbts
   [(prep_pbt thy "pbl_equ_univ_poly" [] e_pblID
       (["polynomial","univariate","equation"],
         [("#Given" ,["equality e_e","solveFor v_v"]),
diff -r b1f0389ca11f -r 73dc85c025ab src/Tools/isac/Knowledge/PolyMinus.thy
--- a/src/Tools/isac/Knowledge/PolyMinus.thy	Mon Jan 27 13:40:36 2014 +0100
+++ b/src/Tools/isac/Knowledge/PolyMinus.thy	Mon Jan 27 21:49:27 2014 +0100
@@ -499,7 +499,7 @@
   SOME "Probe e_e w_w", 
   [["probe","fuer_bruch"]]));
 *}
-setup {* KEStore_Elems.store_pbts
+setup {* KEStore_Elems.add_pbts
   [(prep_pbt thy "pbl_vereinf_poly" [] e_pblID
       (["polynom","vereinfachen"], [], Erls, NONE, [])),
     (prep_pbt thy "pbl_vereinf_poly_minus" [] e_pblID
diff -r b1f0389ca11f -r 73dc85c025ab src/Tools/isac/Knowledge/RatEq.thy
--- a/src/Tools/isac/Knowledge/RatEq.thy	Mon Jan 27 13:40:36 2014 +0100
+++ b/src/Tools/isac/Knowledge/RatEq.thy	Mon Jan 27 21:49:27 2014 +0100
@@ -194,7 +194,7 @@
   RatEq_prls, SOME "solve (e_e::bool, v_v)",
   [["RatEq","solve_rat_equation"]]));
 *}
-setup {* KEStore_Elems.store_pbts
+setup {* KEStore_Elems.add_pbts
   [(prep_pbt thy "pbl_equ_univ_rat" [] e_pblID
     (["rational","univariate","equation"],
       [("#Given", ["equality e_e","solveFor v_v"]),
diff -r b1f0389ca11f -r 73dc85c025ab src/Tools/isac/Knowledge/Rational.thy
--- a/src/Tools/isac/Knowledge/Rational.thy	Mon Jan 27 13:40:36 2014 +0100
+++ b/src/Tools/isac/Knowledge/Rational.thy	Mon Jan 27 21:49:27 2014 +0100
@@ -896,7 +896,7 @@
   SOME "Simplify t_t", 
   [["simplification","of_rationals"]]));
 *}
-setup {* KEStore_Elems.store_pbts
+setup {* KEStore_Elems.add_pbts
   [(prep_pbt thy "pbl_simp_rat" [] e_pblID
       (["rational","simplification"],
         [("#Given" ,["Term t_t"]),
diff -r b1f0389ca11f -r 73dc85c025ab src/Tools/isac/Knowledge/RootEq.thy
--- a/src/Tools/isac/Knowledge/RootEq.thy	Mon Jan 27 13:40:36 2014 +0100
+++ b/src/Tools/isac/Knowledge/RootEq.thy	Mon Jan 27 21:49:27 2014 +0100
@@ -523,7 +523,7 @@
   RootEq_prls,  SOME "solve (e_e::bool, v_v)",
   [["RootEq","norm_sq_root_equation"]]));
 *}
-setup {* KEStore_Elems.store_pbts
+setup {* KEStore_Elems.add_pbts
   [(prep_pbt thy "pbl_equ_univ_root" [] e_pblID
       (["root'","univariate","equation"],
         [("#Given" ,["equality e_e","solveFor v_v"]),
diff -r b1f0389ca11f -r 73dc85c025ab src/Tools/isac/Knowledge/RootRatEq.thy
--- a/src/Tools/isac/Knowledge/RootRatEq.thy	Mon Jan 27 13:40:36 2014 +0100
+++ b/src/Tools/isac/Knowledge/RootRatEq.thy	Mon Jan 27 21:49:27 2014 +0100
@@ -150,7 +150,7 @@
   RootRatEq_prls, SOME "solve (e_e::bool, v_v)",
   [["RootRatEq","elim_rootrat_equation"]]));
 *}
-setup {* KEStore_Elems.store_pbts
+setup {* KEStore_Elems.add_pbts
   [(prep_pbt thy "pbl_equ_univ_root_sq_rat" [] e_pblID
       (["rat","sq","root'","univariate","equation"],
         [("#Given" ,["equality e_e","solveFor v_v"]),
diff -r b1f0389ca11f -r 73dc85c025ab src/Tools/isac/Knowledge/Simplify.thy
--- a/src/Tools/isac/Knowledge/Simplify.thy	Mon Jan 27 13:40:36 2014 +0100
+++ b/src/Tools/isac/Knowledge/Simplify.thy	Mon Jan 27 21:49:27 2014 +0100
@@ -48,7 +48,7 @@
   SOME "Vereinfache t_t", 
   []));
 *}
-setup {* KEStore_Elems.store_pbts
+setup {* KEStore_Elems.add_pbts
   [(prep_pbt thy "pbl_simp" [] e_pblID
       (["simplification"],
         [("#Given" ,["Term t_t"]),
diff -r b1f0389ca11f -r 73dc85c025ab src/Tools/isac/Knowledge/Test.thy
--- a/src/Tools/isac/Knowledge/Test.thy	Mon Jan 27 13:40:36 2014 +0100
+++ b/src/Tools/isac/Knowledge/Test.thy	Mon Jan 27 21:49:27 2014 +0100
@@ -570,7 +570,7 @@
  ------ 25.8.01*)
 
 *}
-setup {* KEStore_Elems.store_pbts
+setup {* KEStore_Elems.add_pbts
   [(prep_pbt thy "pbl_test" [] e_pblID (["test"], [], e_rls, NONE, [])),
     (prep_pbt thy "pbl_test_equ" [] e_pblID
       (["equation","test"],
@@ -831,7 +831,7 @@
 *)
 
 *}
-setup {* KEStore_Elems.store_pbts
+setup {* KEStore_Elems.add_pbts
   [(prep_pbt thy "pbl_test_uni_plain2" [] e_pblID
     (["plain_square","univariate","equation","test"],
       [("#Given" ,["equality e_e","solveFor v_v"]),
@@ -921,7 +921,7 @@
 *)
 
 *}
-setup {* KEStore_Elems.store_pbts
+setup {* KEStore_Elems.add_pbts
   [(prep_pbt thy "pbl_test_uni_poly" [] e_pblID
       (["polynomial","univariate","equation","test"],
         [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
diff -r b1f0389ca11f -r 73dc85c025ab test/Tools/isac/ADDTESTS/accumulate-val/Thy_1.thy
--- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_1.thy	Mon Jan 27 13:40:36 2014 +0100
+++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_1.thy	Mon Jan 27 21:49:27 2014 +0100
@@ -1,19 +1,19 @@
 theory Thy_1 imports Lucas_Interpreter begin
 
 ML {* 
-  (* CHECK length (KEStore_Elems.get_rlss @{theory}) = length (! ruleset') 
+  (* CHECK length (Test_KEStore_Elems.get_rlss @{theory}) = length (! ruleset') 
     AT THE BOTTOM OF A THEORY:*)
-  length (KEStore_Elems.get_rlss @{theory}) = 0;
+  length (Test_KEStore_Elems.get_rlss @{theory}) = 0;
 (*length (! test_ruleset')                  = 1 (* if you have clicked somewhere below *)*)
 *}
-setup {* KEStore_Elems.add_rlss [("test_list_rls", (Context.theory_name @{theory}, Erls))] *}
+setup {* Test_KEStore_Elems.add_rlss [("test_list_rls", (Context.theory_name @{theory}, Erls))] *}
 ML {* 
 (*test_ruleset' := overwritelthy @{theory} (! test_ruleset', [("test_list_rls", Erls)])
   ;
-  if length (KEStore_Elems.get_rlss @{theory}) = length (! test_ruleset') then ()
-    else error "removal of Unsynchonized.ref: ruleset' <> KEStore_Elems.get_rlss in Thy_1"*)
+  if length (Test_KEStore_Elems.get_rlss @{theory}) = length (! test_ruleset') then ()
+    else error "removal of Unsynchonized.ref: ruleset' <> Test_KEStore_Elems.get_rlss in Thy_1"*)
 *}
 
-setup {* KEStore_Elems.add_calcs [("calc", ("Thy_1", e_evalfn))] *}
+setup {* Test_KEStore_Elems.add_calcs [("calc", ("Thy_1", e_evalfn))] *}
 
 end
diff -r b1f0389ca11f -r 73dc85c025ab test/Tools/isac/ADDTESTS/accumulate-val/Thy_2.thy
--- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_2.thy	Mon Jan 27 13:40:36 2014 +0100
+++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_2.thy	Mon Jan 27 21:49:27 2014 +0100
@@ -3,7 +3,7 @@
 ML {* val test_list_rls =
   append_rls "test_list_rls" e_rls [Thm ("refl", @{thm refl}), Thm ("subst", @{thm subst})] *}
 
-setup {* KEStore_Elems.add_rlss 
+setup {* Test_KEStore_Elems.add_rlss 
   [("test_list_rls", (Context.theory_name @{theory}, (*already added in Thy_1.thy*)
     test_list_rls))] *}
 
diff -r b1f0389ca11f -r 73dc85c025ab test/Tools/isac/ADDTESTS/accumulate-val/Thy_2b.thy
--- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_2b.thy	Mon Jan 27 13:40:36 2014 +0100
+++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_2b.thy	Mon Jan 27 21:49:27 2014 +0100
@@ -3,7 +3,7 @@
 ML {* val test_list_rls =
   append_rls "test_list_rls" e_rls [Thm ("False_def", @{thm False_def})] *}
 
-setup {* KEStore_Elems.add_rlss [("test_list_rls", (Context.theory_name @{theory},
+setup {* Test_KEStore_Elems.add_rlss [("test_list_rls", (Context.theory_name @{theory},
   test_list_rls))] *}
 ML {* (*test_ruleset' := overwritelthy @{theory} (! test_ruleset', 
   [("test_list_rls", test_list_rls)])*)
diff -r b1f0389ca11f -r 73dc85c025ab test/Tools/isac/ADDTESTS/accumulate-val/Thy_3.thy
--- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_3.thy	Mon Jan 27 13:40:36 2014 +0100
+++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_3.thy	Mon Jan 27 21:49:27 2014 +0100
@@ -3,27 +3,27 @@
 ML {* val test_list_rls =
   append_rls "test_list_rls" e_rls [Thm ("not_def", @{thm not_def})] *}
 
-setup {* KEStore_Elems.add_rlss (*already added in Thy_1.thy and Thy_2.thy*)
+setup {* Test_KEStore_Elems.add_rlss (*already added in Thy_1.thy and Thy_2.thy*)
   [("test_list_rls", (Context.theory_name @{theory}, test_list_rls))] *}
 
 ML {*
-  if length (KEStore_Elems.get_rlss @{theory}) = 1 (*stored in 3 different theories*)
+  if length (Test_KEStore_Elems.get_rlss @{theory}) = 1 (*stored in 3 different theories*)
   then () else error "rls identified by string-identifier, not by theory: changed"
 
 (*test_ruleset' := overwritelthy @{theory} (! test_ruleset', [("test_list_rls", 
     append_rls "test_list_rls" test_list_rls [Calc ("test_function", e_evalfn)])])*)
   ;
-(*if length (KEStore_Elems.get_rlss @{theory}) = length (! test_ruleset')
-  then () else error "KEStore_Elems.get_rlss = test_ruleset': changed"*)
+(*if length (Test_KEStore_Elems.get_rlss @{theory}) = length (! test_ruleset')
+  then () else error "Test_KEStore_Elems.get_rlss = test_ruleset': changed"*)
   ;
   val SOME (_, Rls {rules, ...}) =
-    AList.lookup op= (KEStore_Elems.get_rlss @{theory}) "test_list_rls"
+    AList.lookup op= (Test_KEStore_Elems.get_rlss @{theory}) "test_list_rls"
   ;
   case rules of
     [Thm ("not_def", _)] => ()
   | _ => error "union rls_eq changed: 1st argument is NOT overwritten anymore"
   (* merge rules of rls with the same identifier rls' must be done one level higher:
-    KEStore_Elems.add_rlss does *add* or *overwrite* *)
+    Test_KEStore_Elems.add_rlss does *add* or *overwrite* *)
 *}
 
 end
diff -r b1f0389ca11f -r 73dc85c025ab test/Tools/isac/ADDTESTS/accumulate-val/Thy_4.thy
--- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_4.thy	Mon Jan 27 13:40:36 2014 +0100
+++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_4.thy	Mon Jan 27 21:49:27 2014 +0100
@@ -1,5 +1,5 @@
 theory Thy_4 imports Lucas_Interpreter (*!!!!!*) begin
 
-setup {* KEStore_Elems.add_rlss [("rls1", ("Thy_4", Erls)), ("rls2", ("Thy_4", Erls))] *}
+setup {* Test_KEStore_Elems.add_rlss [("rls1", ("Thy_4", Erls)), ("rls2", ("Thy_4", Erls))] *}
 
 end
diff -r b1f0389ca11f -r 73dc85c025ab test/Tools/isac/ADDTESTS/accumulate-val/Thy_5.thy
--- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_5.thy	Mon Jan 27 13:40:36 2014 +0100
+++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_5.thy	Mon Jan 27 21:49:27 2014 +0100
@@ -1,5 +1,5 @@
 theory Thy_5 imports Thy_4 begin
 
-setup {* KEStore_Elems.add_rlss [("rls", ("Thy_5", Erls))] *}
+setup {* Test_KEStore_Elems.add_rlss [("rls", ("Thy_5", Erls))] *}
 
 end                             
diff -r b1f0389ca11f -r 73dc85c025ab test/Tools/isac/ADDTESTS/accumulate-val/Thy_All.thy
--- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_All.thy	Mon Jan 27 13:40:36 2014 +0100
+++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_All.thy	Mon Jan 27 21:49:27 2014 +0100
@@ -1,7 +1,7 @@
 theory Thy_All imports Thy_3 Thy_5 begin
 
 ML {*
-KEStore_Elems.get_rlss @{theory}
+Test_KEStore_Elems.get_rlss @{theory}
 (*|> map check_kestore_rls 
   |> enumerate_strings
   |> map writeln*)
@@ -12,13 +12,13 @@
 (test_list_rls, (Thy_3, Rls {#calc = 0, #rules = 1, ...))--4 
 *)
 ;
-case KEStore_Elems.get_rlss @{theory} of
+case Test_KEStore_Elems.get_rlss @{theory} of
   ("rls2", ("Thy_4", Erls)) :: ("rls1", ("Thy_4", Erls)) :: _ => ()
-| _ => raise error "KEStore_Elems.get_rlss changed"
+| _ => raise error "Test_KEStore_Elems.get_rlss changed"
 ;
-case KEStore_Elems.get_calcs @{theory} of
+case Test_KEStore_Elems.get_calcs @{theory} of
   [("calc", ("Thy_1", _))] => ()
-| _ => raise error "KEStore_Elems.get_calcs changed"
+| _ => raise error "Test_KEStore_Elems.get_calcs changed"
 *}
 
 end
diff -r b1f0389ca11f -r 73dc85c025ab test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml
--- a/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml	Mon Jan 27 13:40:36 2014 +0100
+++ b/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml	Mon Jan 27 21:49:27 2014 +0100
@@ -14,7 +14,7 @@
   (*etc*)
 end;                               
 
-structure KEStore_Elems: KESTORE_ELEMS =
+structure Test_KEStore_Elems: KESTORE_ELEMS =
 struct
   fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
 
diff -r b1f0389ca11f -r 73dc85c025ab test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy
--- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Mon Jan 27 13:40:36 2014 +0100
+++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Mon Jan 27 21:49:27 2014 +0100
@@ -892,7 +892,7 @@
    (prep_pbt thy "pbl_SP_Ztrans" [] e_pblID
    (["Z_Transform","SignalProcessing"], [], e_rls, NONE, []));
 *}
-setup {* store_pbts
+setup {* KEStore_Elems.add_pbts
   [prep_pbt thy "pbl_SP" [] e_pblID (["SignalProcessing"], [], e_rls, NONE, []),
     prep_pbt thy "pbl_SP_Ztrans" [] e_pblID
       (["Z_Transform","SignalProcessing"], [], e_rls, NONE, [])] *}
@@ -911,7 +911,7 @@
     append_rls "e_rls" e_rls [(*for preds in where_*)], NONE, 
     [["SignalProcessing","Z_Transform","Inverse"]]));
 *}
-setup {* store_pbts
+setup {* KEStore_Elems.add_pbts
   [prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID
       (["Inverse", "Z_Transform", "SignalProcessing"],
         [("#Given", ["filterExpression X_eq"]),
diff -r b1f0389ca11f -r 73dc85c025ab test/Tools/isac/Interpret/rewtools.sml
--- a/test/Tools/isac/Interpret/rewtools.sml	Mon Jan 27 13:40:36 2014 +0100
+++ b/test/Tools/isac/Interpret/rewtools.sml	Mon Jan 27 21:49:27 2014 +0100
@@ -73,12 +73,12 @@
 val isabthms = (flat o (map Theory.axioms_of)) ancestors;
 
 val isacrules = (flat o (map (thms_of_rls o #2 o #2))) 
-  (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"));
+  (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"));
 (*thms from rulesets*)
 (*=== inhibit exn AK110725 =============================================================
 val isacrlsthms = ((map rep_thm_G') o flat o 
 		 (map (PureThy.all_thms_of_rls o #2 o #2))) 
-		   (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"));
+		   (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"));
 length isacrlsthms;
 (*takes a few seconds...
 val isacrlsthms = gen_distinct eq_thmI isacrlsthms;
@@ -159,14 +159,14 @@
 curry ((op mem) o swap) dropthys' "Isac";
 		val ancestors_rls = 
 		  filter_out ((curry ((op mem) o swap) dropthys') o ((#1 o #2): rls'*(theory' * rls)->theory'))
-		     (rev (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")));
+		     (rev (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")));
 
 take (10, map #1 ancestors_rls) = 
   ["expand_binomtest", "make_polytest", "rearrange_assoc", "ac_plus_times", "norm_equation", 
    "matches", "isolate_bdv", "isolate_root", "tval_rls", "Test_simplify"]; (*..all rls in each*)
 
 (* WN120523 popped up again ?!?!?
-if length (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")) <> length ancestors_rls then ()
+if length (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")) <> length ancestors_rls then ()
 else error "rewtools.sml: diff.behav. in thy_containing_rls 2 ERRATICAL?";
 *)
 
@@ -191,7 +191,7 @@
     val dropthys' = map (get_thy o (#1 : (theory' * theory) -> theory')) dropthys: string list;
 		    val ancestors_rls = 
 		      filter_out ((curry ((op mem) o swap) dropthys') o ((#1 o #2): rls'*(theory' * rls)->theory'))
-		        (rev (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")));
+		        (rev (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")));
 		
 case assoc (ancestors_rls, rls') of
   SOME ("Poly", Seq {id = "norm_Poly", ...}) => ()
@@ -218,13 +218,13 @@
   "LinEq", "Root", "Equation", "Rational", "Poly", "Simplify"] (*, "Atools", ..*)
 then () else error "thy_containing_cal changed ancestors_rls for Atools";
 
-Thy_Info.get_theory thy' |> KEStore_Elems.get_calcs |> rev;
-Thy_Info.get_theory thy' |> KEStore_Elems.get_calcs |> rev |> map #1;
-Thy_Info.get_theory thy' |> KEStore_Elems.get_calcs |> rev |> map (#1 : calc -> string);
+Thy_Info.get_theory thy' |> Test_KEStore_Elems.get_calcs |> rev;
+Thy_Info.get_theory thy' |> Test_KEStore_Elems.get_calcs |> rev |> map #1;
+Thy_Info.get_theory thy' |> Test_KEStore_Elems.get_calcs |> rev |> map (#1 : calc -> string);
 
     val ancestors_cal =
       filter_out ((curry ((op mem) o swap) dropthys') o (#1 : calc -> string))
-        (Thy_Info.get_theory thy' |> KEStore_Elems.get_calcs |> rev);
+        (Thy_Info.get_theory thy' |> Test_KEStore_Elems.get_calcs |> rev);
 
 if thy_containing_cal "Biegelinie" "PLUS" = ("IsacKnowledge", "plus") 
                     (*WN120410: SHOULD BE = ("IsacKnowledge", "Atools")*)
diff -r b1f0389ca11f -r 73dc85c025ab test/Tools/isac/Knowledge/build_thydata.sml
--- a/test/Tools/isac/Knowledge/build_thydata.sml	Mon Jan 27 13:40:36 2014 +0100
+++ b/test/Tools/isac/Knowledge/build_thydata.sml	Mon Jan 27 21:49:27 2014 +0100
@@ -30,14 +30,14 @@
 
 local
     val isacrlsthms = ((gen_distinct eq_thmI) o (map rep_thm_G') o flat o 
-		       (map (thms_of_rls o #2 o #2))) (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"));
+		       (map (thms_of_rls o #2 o #2))) (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"));
     val isacthms = (flat o (map (thms_of o #2))) (!theory');
 in
     val rlsthmsNOTisac = gen_diff eq_thmI (isacrlsthms, isacthms);
 end;
 *)
     val isacrlsthms''''' = ((gen_distinct eq_thmI) o (map rep_thm_G') o flat o 
-		       (map (thms_of_rls o #2 o #2))) (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"))
+		       (map (thms_of_rls o #2 o #2))) (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"))
 		         :  (thmID * thm) list;
 (* THIS IS TOO EXPENSIVE:
 val all_ListC_thms = Global_Theory.all_thms_of (@{theory "ListC"});
@@ -137,7 +137,7 @@
 "-------- prop_of thm .. Theory.axioms_of ---------------";
 "-------- prop_of thm .. Theory.axioms_of ---------------";
 "-------- prop_of thm .. Theory.axioms_of ---------------";
-val isacrlsthms''''' = (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"))
+val isacrlsthms''''' = (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"))
   |> map (thms_of_rls o #2 o #2) (*drop manually input id in Thm (id, thm)*)
   |> flat
   |> map thm_of_thm
@@ -247,7 +247,7 @@
 "----- so we cannot get isacthms as thm, only as term ---";
 "----- but we can retain isacrlsthms as thm ---";
 *)
-val isacrlsthms = (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"))
+val isacrlsthms = (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"))
   |> map (thms_of_rls o #2 o #2) (*drop manually input id in Thm (id, thm)*)
   |> flat
   |> map thm_of_thm
diff -r b1f0389ca11f -r 73dc85c025ab test/Tools/isac/OLDTESTS/script_if.sml
--- a/test/Tools/isac/OLDTESTS/script_if.sml	Mon Jan 27 13:40:36 2014 +0100
+++ b/test/Tools/isac/OLDTESTS/script_if.sml	Mon Jan 27 21:49:27 2014 +0100
@@ -65,7 +65,7 @@
 			  eval_is_rootequation_in "")],
   [("Test","methode")]));
 
-store_pbts
+Test_KEStore_Elems.add_pbts
   [prep_pbt (*Test.thy*) (theory "Isac")
       (["root'","univariate","equation","test"],
         [("#Given" ,["equality e_e","solveFor v_v"]),
@@ -90,7 +90,7 @@
   append_rls e_rls [Calc ("Tools.matches",eval_matches "#matches_")],
   []));
 
-store_pbts
+Test_KEStore_Elems.add_pbts
   [prep_pbt (theory "Isac")
       (["approximate","univariate","equation","test"],
         [("#Given", ["equality e_e","solveFor v_v","errorBound err_"]),
diff -r b1f0389ca11f -r 73dc85c025ab test/Tools/isac/OLDTESTS/scriptnew.sml
--- a/test/Tools/isac/OLDTESTS/scriptnew.sml	Mon Jan 27 13:40:36 2014 +0100
+++ b/test/Tools/isac/OLDTESTS/scriptnew.sml	Mon Jan 27 21:49:27 2014 +0100
@@ -32,7 +32,7 @@
   ],
   e_rls, NONE, []));
 
-store_pbts
+Test_KEStore_Elems.add_pbts
   [prep_pbt Test.thy "pbl_testss" [] e_pblID
       (["tests"], []:(string * string list) list, e_rls, NONE, []),
     prep_pbt Test.thy "pbl_testss_term" [] e_pblID
@@ -109,7 +109,7 @@
    ("#Find"  ,["boolTestFind v_i_"])
   ],
   e_rls, NONE, []));
-store_pbts
+Test_KEStore_Elems.add_pbts
   [prep_pbt Test.thy "pbl_testss_eq" [] e_pblID
       (["met_testeq","tests"],
         [("#Given" ,["boolTestGiven e_e"]),
diff -r b1f0389ca11f -r 73dc85c025ab test/Tools/isac/Test_Isac.thy
--- a/test/Tools/isac/Test_Isac.thy	Mon Jan 27 13:40:36 2014 +0100
+++ b/test/Tools/isac/Test_Isac.thy	Mon Jan 27 21:49:27 2014 +0100
@@ -45,20 +45,39 @@
   ML {*"%%%%%%%%%%%%%%%%% end Isabelle %%%%%%%%%%%%%%%%%%%%%%%%%";*}
 
 section {* test ML Code of isac *}
+  setup {* KEStore_Elems.add_pbts
+    [prep_pbt @{theory "Test"} "pbl_ttest" [] e_pblID (["test"], [], e_rls, NONE, []),
+      prep_pbt @{theory "Test"} "pbl_ttest_calc" [] e_pblID
+        (["calculate","test"],
+          [("#Given" ,["realTestGiven t_t"]),
+            ("#Find"  ,["realTestFind s_s"])],
+          e_rls, NONE, [["Test","test_calculate"]]),
+       prep_pbt thy "pbl_test_refine" [] e_pblID (["refine", "test"], [], e_rls, NONE, []),
+       prep_pbt @{theory DiffApp} "pbl_pbla" [] e_pblID
+         (["pbla", "refine", "test"], [("#Given", ["fixedValues a_a"])], e_rls, NONE, []),
+       prep_pbt @{theory DiffApp} "pbl_pbla1" [] e_pblID
+         (["pbla1","pbla", "refine", "test"],
+           [("#Given", ["fixedValues a_a","maximum a_1"])], e_rls, NONE, []),
+       prep_pbt @{theory DiffApp} "pbl_pbla2" [] e_pblID
+         (["pbla2","pbla", "refine", "test"], 
+           [("#Given", ["fixedValues a_a","valuesFor a_2"])], e_rls, NONE, []),
+       prep_pbt @{theory DiffApp} "pbl_pbla2x" [] e_pblID
+         (["pbla2x","pbla2","pbla", "refine", "test"],
+           [("#Given", ["fixedValues a_a","valuesFor a_2","functionOf a2_x"])], e_rls, NONE, []),
+       prep_pbt @{theory DiffApp} "pbl_pbla2y" [] e_pblID
+         (["pbla2y","pbla2","pbla", "refine", "test"],
+           [("#Given" ,["fixedValues a_a","valuesFor a_2","boundVariable a2_y"])], e_rls, NONE, []),
+       prep_pbt @{theory DiffApp} "pbl_pbla2z" [] e_pblID
+         (["pbla2z","pbla2","pbla", "refine", "test"],
+           [("#Given" ,["fixedValues a_a","valuesFor a_2","interval a2_z"])], e_rls, NONE, []),
+       prep_pbt @{theory DiffApp} "pbl_pbla3" [] e_pblID
+         (["pbla3","pbla", "refine", "test"],
+           [("#Given" ,["fixedValues a_a","relations a_3"])], e_rls, NONE, [])] *}
   ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*}
   ML_file          "library.sml"
   ML_file          "calcelems.sml"
   ML_file          "kestore.sml"
   ML_file "ProgLang/termC.sml"
-
-  setup {* store_pbts
-    [prep_pbt @{theory "Test"} "pbl_ttest" [] e_pblID (["test"], [], e_rls, NONE, []),
-      prep_pbt @{theory "Test"} "pbl_ttest_calc" [] e_pblID
-        (["calculate","test"],
-          [("#Given" ,["realTestGiven t_t"]),
-            ("#Find"  ,["realTestFind s_s"])],
-          e_rls, NONE, [["Test","test_calculate"]])] *}
-
   ML_file "ProgLang/calculate.sml"
   ML_file "ProgLang/rewrite.sml"
   ML_file "ProgLang/listC.sml"
diff -r b1f0389ca11f -r 73dc85c025ab test/Tools/isac/kestore.sml
--- a/test/Tools/isac/kestore.sml	Mon Jan 27 13:40:36 2014 +0100
+++ b/test/Tools/isac/kestore.sml	Mon Jan 27 21:49:27 2014 +0100
@@ -8,7 +8,7 @@
 "table of contents -----------------------------------------------------------";
 "-----------------------------------------------------------------------------";
 "-------- fun check_kestore_rls ----------------------------------------------";
-"-------- fun KEStore_Elems.add_rlss overwrites earlier data -----------------";
+"-------- fun Test_KEStore_Elems.add_rlss overwrites earlier data ------------";
 "-----------------------------------------------------------------------------";
 "-----------------------------------------------------------------------------";
 
@@ -19,16 +19,16 @@
   "(e_rls, (KEStore, Rls {#calc = 0, #rules = 0, ...))"
 then () else error "check_kestore_rls changed"
 ;
-KEStore_Elems.get_rlss @{theory Isac} 
+Test_KEStore_Elems.get_rlss @{theory Isac} 
   |> map check_kestore_rls 
   |> enumerate_strings
   |> sort string_ord
 (*|> map writeln*)
 ;
 
-"-------- fun KEStore_Elems.add_rlss overwrites earlier data -----------------";
-"-------- fun KEStore_Elems.add_rlss overwrites earlier data -----------------";
-"-------- fun KEStore_Elems.add_rlss overwrites earlier data -----------------";
+"-------- fun Test_KEStore_Elems.add_rlss overwrites earlier data -----------------";
+"-------- fun Test_KEStore_Elems.add_rlss overwrites earlier data -----------------";
+"-------- fun Test_KEStore_Elems.add_rlss overwrites earlier data -----------------";
   fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
   fun rls_eq ((id1, (thyID1, _)), (id2, (thyID2, _))) = id1 = id2 (*andalso thyID1 = thyID2*)
 
diff -r b1f0389ca11f -r 73dc85c025ab test/Tools/isac/xmlsrc/thy-hierarchy.sml
--- a/test/Tools/isac/xmlsrc/thy-hierarchy.sml	Mon Jan 27 13:40:36 2014 +0100
+++ b/test/Tools/isac/xmlsrc/thy-hierarchy.sml	Mon Jan 27 21:49:27 2014 +0100
@@ -38,7 +38,7 @@
 overwrite (al, b);
 overwritelthy thy (al, bl);
 
-case assoc' ((KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")),"e_rls") of
+case assoc' ((Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")),"e_rls") of
   SOME ("Tools", Rls _) => ()
 | _ => error "e_rls not in Theory_Data" 
 
@@ -80,7 +80,7 @@
 val thy' = "Test";
 val rlss = filter ((curry op= thy') o 
 			   ((#1 o #2):(rls' * (theory' * rls)) -> theory')) 
-			  (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"));
+			  (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"));
 collect_rlss ("IsacKnowledge",thy');
 
 "collect_thy thy-------------------------------------------------";
@@ -388,7 +388,7 @@
     val dropthys' = map (get_thy o (#1 : (theory' * theory) -> theory')) dropthys: string list;
 		    val ancestors_rls = 
 		      filter_out ((curry ((op mem) o swap) dropthys') o ((#1 o #2): rls'*(theory' * rls)->theory'))
-		        (rev (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")));
+		        (rev (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")));
 
 case assoc (ancestors_rls, rls') of
   SOME ("Poly", Rls {id = "discard_minus", ...}) => ()