test/Tools/isac/xmlsrc/thy-hierarchy.sml
changeset 55359 73dc85c025ab
parent 52156 aa0884017d48
child 55397 71f7fd375e7d
     1.1 --- a/test/Tools/isac/xmlsrc/thy-hierarchy.sml	Mon Jan 27 13:40:36 2014 +0100
     1.2 +++ b/test/Tools/isac/xmlsrc/thy-hierarchy.sml	Mon Jan 27 21:49:27 2014 +0100
     1.3 @@ -38,7 +38,7 @@
     1.4  overwrite (al, b);
     1.5  overwritelthy thy (al, bl);
     1.6  
     1.7 -case assoc' ((KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")),"e_rls") of
     1.8 +case assoc' ((Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")),"e_rls") of
     1.9    SOME ("Tools", Rls _) => ()
    1.10  | _ => error "e_rls not in Theory_Data" 
    1.11  
    1.12 @@ -80,7 +80,7 @@
    1.13  val thy' = "Test";
    1.14  val rlss = filter ((curry op= thy') o 
    1.15  			   ((#1 o #2):(rls' * (theory' * rls)) -> theory')) 
    1.16 -			  (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"));
    1.17 +			  (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"));
    1.18  collect_rlss ("IsacKnowledge",thy');
    1.19  
    1.20  "collect_thy thy-------------------------------------------------";
    1.21 @@ -388,7 +388,7 @@
    1.22      val dropthys' = map (get_thy o (#1 : (theory' * theory) -> theory')) dropthys: string list;
    1.23  		    val ancestors_rls = 
    1.24  		      filter_out ((curry ((op mem) o swap) dropthys') o ((#1 o #2): rls'*(theory' * rls)->theory'))
    1.25 -		        (rev (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")));
    1.26 +		        (rev (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")));
    1.27  
    1.28  case assoc (ancestors_rls, rls') of
    1.29    SOME ("Poly", Rls {id = "discard_minus", ...}) => ()