1.1 --- a/test/Tools/isac/Knowledge/build_thydata.sml	Mon Jan 27 13:40:36 2014 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/build_thydata.sml	Mon Jan 27 21:49:27 2014 +0100
     1.3 @@ -30,14 +30,14 @@
     1.4  
     1.5  local
     1.6      val isacrlsthms = ((gen_distinct eq_thmI) o (map rep_thm_G') o flat o 
     1.7 -		       (map (thms_of_rls o #2 o #2))) (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"));
     1.8 +		       (map (thms_of_rls o #2 o #2))) (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"));
     1.9      val isacthms = (flat o (map (thms_of o #2))) (!theory');
    1.10  in
    1.11      val rlsthmsNOTisac = gen_diff eq_thmI (isacrlsthms, isacthms);
    1.12  end;
    1.13  *)
    1.14      val isacrlsthms''''' = ((gen_distinct eq_thmI) o (map rep_thm_G') o flat o 
    1.15 -		       (map (thms_of_rls o #2 o #2))) (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"))
    1.16 +		       (map (thms_of_rls o #2 o #2))) (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"))
    1.17  		         :  (thmID * thm) list;
    1.18  (* THIS IS TOO EXPENSIVE:
    1.19  val all_ListC_thms = Global_Theory.all_thms_of (@{theory "ListC"});
    1.20 @@ -137,7 +137,7 @@
    1.21  "-------- prop_of thm .. Theory.axioms_of ---------------";
    1.22  "-------- prop_of thm .. Theory.axioms_of ---------------";
    1.23  "-------- prop_of thm .. Theory.axioms_of ---------------";
    1.24 -val isacrlsthms''''' = (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"))
    1.25 +val isacrlsthms''''' = (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"))
    1.26    |> map (thms_of_rls o #2 o #2) (*drop manually input id in Thm (id, thm)*)
    1.27    |> flat
    1.28    |> map thm_of_thm
    1.29 @@ -247,7 +247,7 @@
    1.30  "----- so we cannot get isacthms as thm, only as term ---";
    1.31  "----- but we can retain isacrlsthms as thm ---";
    1.32  *)
    1.33 -val isacrlsthms = (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"))
    1.34 +val isacrlsthms = (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"))
    1.35    |> map (thms_of_rls o #2 o #2) (*drop manually input id in Thm (id, thm)*)
    1.36    |> flat
    1.37    |> map thm_of_thm