1.1 --- a/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml	Sun Apr 19 11:07:02 2020 +0200
     1.2 +++ b/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml	Sun Apr 19 12:22:37 2020 +0200
     1.3 @@ -90,14 +90,14 @@
     1.4  "----------- search for data error in thes2file ------------------";
     1.5  "----------- search for data error in thes2file ------------------";
     1.6  val TESTdump = Unsynchronized.ref 
     1.7 -  ("path": filepath, ["ids"]: theID, []: pos, thydata2file, Ptyp ("xxx", [], []): thydata ptyp);
     1.8 +  ("path": filepath, ["ids"]: theID, []: pos, thydata2file, Celem1.Ptyp ("xxx", [], []): thydata Celem1.ptyp);
     1.9  
    1.10 -fun TESTthenode (pa:filepath) ids po wfn (Ptyp (id, [n], ns)) TESTids = 
    1.11 +fun TESTthenode (pa:filepath) ids po wfn (Celem1.Ptyp (id, [n], ns)) TESTids = 
    1.12      let val po' = lev_on po
    1.13      in 
    1.14        if (ids@[id]) = TESTids
    1.15        then
    1.16 -        (TESTdump := (pa, ids, po', wfn, (Ptyp (id, [n], ns))); 
    1.17 +        (TESTdump := (pa, ids, po', wfn, (Celem1.Ptyp (id, [n], ns))); 
    1.18            error "stopped before error, created TESTdump") (* this exn creates right signature*)
    1.19        else
    1.20          wfn pa po' (ids @ [id]) n; TESTthenodes pa (ids @ [id]) ((lev_dn po'): pos) wfn ns TESTids
    1.21 @@ -120,7 +120,7 @@
    1.22  handle _(* "stopped before error, created TESTdump" *) => ());
    1.23  ;
    1.24  (* /----- uncomment in case of "data error in thes2file" ----------------------------(*1*)-----\*)
    1.25 -val (pa, ids, po', wfn, (Ptyp (id, [n], ns))) = ! TESTdump; 
    1.26 +val (pa, ids, po', wfn, (Celem1.Ptyp (id, [n], ns))) = ! TESTdump; 
    1.27  ;
    1.28  "~~~~~ fun thydata2file, args:"; val ((xmldata:filepath), (pos:pos), (theID:theID), thydata) =
    1.29    (pa, po', (ids@[id]), n);
    1.30 @@ -160,12 +160,12 @@
    1.31  "----------- correct theIDs for Rule_Set.empty ----------------------------";
    1.32  "----------- correct theIDs for Rule_Set.empty ----------------------------";
    1.33  "----------- correct theIDs for Rule_Set.empty ----------------------------";
    1.34 -if thy_containing_rls "Build_Thydata" "empty" = ("IsacScripts", "KEStore") then ()
    1.35 +if thy_containing_rls "Build_Thydata" "empty" = ("IsacScripts", "Know_Store") then ()
    1.36  else error "thy_containing_rls Rule_Set.empty changed";
    1.37  show_thes ();
    1.38  (*shows different assignment for "empty"...
    1.39    : 
    1.40 -                                                ["IsacScripts", "KEStore", "Rulesets", "empty"], 
    1.41 +                                                ["IsacScripts", "Know_Store", "Rulesets", "empty"], 
    1.42    :*)
    1.43  
    1.44  "----------- fun revert_sym_rule --------------------------------------";
    1.45 @@ -188,7 +188,7 @@
    1.46  "----------- fun thms_of_rlss ------------------------------------";
    1.47  "----------- fun thms_of_rlss ------------------------------------";
    1.48  val rlss = 
    1.49 -  [("empty" : Rule_Set.id, ("KEStore": ThyC.id, Rule_Set.empty)),
    1.50 +  [("empty" : Rule_Set.id, ("Know_Store": ThyC.id, Rule_Set.empty)),
    1.51    ("discard_minus" : Rule_Set.id, ("Poly": ThyC.id, discard_minus))]
    1.52  ;
    1.53  val [_, (thmID, term)] = thms_of_rlss thy rlss;
    1.54 @@ -322,7 +322,7 @@
    1.55      mathauthors = ["isac-team"], thm = _})] => ()
    1.56  | _ => error "collect thydata from Test_Build_Thydata changed";
    1.57  ;
    1.58 -(* we store locally on MINIthehier instead on KEStore, see KEStore: *)
    1.59 +(* we store locally on MINIthehier instead on Know_Store, see Know_Store: *)
    1.60      fun add_the (thydata, theID) = add_thydata ([], theID) thydata;
    1.61  val thes = map (fn (a, b) => (b, a)) thydata_list
    1.62  val MINIthehier = (fold add_the thes) (KEStore_Elems.get_thes @{theory Test_Build_Thydata});
    1.63 @@ -361,7 +361,7 @@
    1.64  "~~~~~ fun MINIthes2file, args:"; val (path) = ("/tmp/");
    1.65  "~~~~~ and thenodes, args:"; val (pa, ids, po, wfn, (n::ns)) = 
    1.66    (path, [], [0], thydata2file, MINIthehier);
    1.67 -"~~~~~ fun thenode, args:"; val ((pa : filepath), ids, po, wfn, (Ptyp (id, [n], ns))) = 
    1.68 +"~~~~~ fun thenode, args:"; val ((pa : filepath), ids, po, wfn, (Celem1.Ptyp (id, [n], ns))) = 
    1.69    (pa, ids, po, wfn, n);
    1.70  val po' = lev_on po;
    1.71  (*wfn pa po' (ids @ [id]) n  -------------> writes xml to file; we want xml before written: *)