1.1 --- a/src/Tools/isac/Interpret/rewtools.sml	Thu Jun 19 07:40:46 2014 +0200
     1.2 +++ b/src/Tools/isac/Interpret/rewtools.sml	Thu Jun 19 07:51:40 2014 +0200
     1.3 @@ -653,28 +653,6 @@
     1.4      (tracing ("### atomic_appl_tacs: not impl. for tac = '"^ tac2str tac ^"'");
     1.5       []);
     1.6  
     1.7 -
     1.8 -
     1.9 -
    1.10 -
    1.11 -(*.not only for thydata, but also for thy's etc.*)
    1.12 -fun theID2guh (theID:theID) =
    1.13 -    case length theID of
    1.14 -	0 => error ("theID2guh: called with theID = "^strs2str' theID)
    1.15 -      | 1 => part2guh theID
    1.16 -      | 2 => thy2guh theID
    1.17 -      | 3 => thypart2guh theID
    1.18 -      | 4 => let val [isa, thyID, typ, elemID] = theID
    1.19 -	     in case typ of
    1.20 -		    "Theorems" => thm2guh (isa, thyID) elemID
    1.21 -		  | "Rulesets" => rls2guh (isa, thyID) elemID
    1.22 -		  | "Calculations" => cal2guh (isa, thyID) elemID
    1.23 -		  | "Orders" => ord2guh (isa, thyID) elemID
    1.24 -		  | "Theorems" => thy2guh [isa, thyID]
    1.25 -		  | str => error ("theID2guh: called with theID = "^
    1.26 -					strs2str' theID)
    1.27 -	     end
    1.28 -      | n => error ("theID2guh called with theID = "^strs2str' theID);
    1.29  (*.filenames not only for thydata, but also for thy's etc.*)
    1.30  fun theID2filename (theID:theID) = theID2guh theID ^ ".xml" : filename;
    1.31  

     2.1 --- a/src/Tools/isac/calcelems.sml	Thu Jun 19 07:40:46 2014 +0200
     2.2 +++ b/src/Tools/isac/calcelems.sml	Thu Jun 19 07:51:40 2014 +0200
     2.3 @@ -975,66 +975,6 @@
     2.4  		      "consider setting 'check_guhs_unique := false'")
     2.5      else ();
     2.6  
     2.7 -(* for preserving elements created by 'fun store_thy' *)
     2.8 -fun exist_the (theID : theID) (thy_hie : thehier) =
     2.9 -  let 
    2.10 -    fun node theID ids (Ptyp (id, _, ns)) =
    2.11 -      if theID = ids @ [id] then true else nodes theID (ids @ [id]) ns
    2.12 -    and nodes _ _ [] = false
    2.13 -      | nodes theID ids (n::ns) =
    2.14 -        if node theID ids n then true else nodes theID ids ns
    2.15 -  in nodes theID [] thy_hie end;
    2.16 -
    2.17 -(* insrt requires a parent; see 'fun fill_parents' *)
    2.18 -fun can_insert (theID : theID) (thy_hie : thehier) = 
    2.19 -  (insrt theID e_thydata theID thy_hie; true)
    2.20 -    handle _ => false;
    2.21 -    
    2.22 -(* cut 'theID', the ID of theory elements from tail to head
    2.23 -   until insertion into the hierarchy of theory elements 'th' is possible
    2.24 -   (the hierarchy requires the parentnode to exist for insertion) *)
    2.25 -fun cut_theID th ([] : theID) = error "could not insert into thy-hierarchy"
    2.26 -  | cut_theID th theID  = 
    2.27 -    if can_insert theID th
    2.28 -    then theID else cut_theID th (drop_last theID);
    2.29 -
    2.30 -(* insert empty parents 'Html' into the hierarchy of theory elements 'th'
    2.31 -   until the actual node can be inserted with key 'theID' *)
    2.32 -fun fill_parents th cutID theID =
    2.33 -  let val cutID' = cut_theID th cutID
    2.34 -  in if cutID' = theID
    2.35 -    then th
    2.36 -    else 
    2.37 -      let 
    2.38 -        val th' = insrt cutID' (Html {guh=theID2guh theID, coursedesign = ["isac team 2006"],
    2.39 -          mathauthors = [], html = ""}) cutID' th
    2.40 -        val cutID_ = cutID' @ [nth ((length cutID') + 1) theID]
    2.41 -      in fill_parents th' cutID_ theID end
    2.42 -  end;
    2.43 -
    2.44 -(* argument 1 "th : thehier": contains some thydata from "setup {* KEStore_Elems.add_thes ..."
    2.45 -   argument 1 "th : thehier": contains some thydata from "store_thes ..."
    2.46 -      already in some "ProgLang/*.thy" or "Knowledge/*.thy"
    2.47 -   argument 2 "(theID, thydata)::_ : (theID * thydata) list: contains thydata collected
    2.48 -      automatically in Build_Thydata.thy finally.
    2.49 -   parents of thydata in list, missing in thehier, are inserted 
    2.50 -      (causing msgs '*** insert: not found');
    2.51 -   (1) is kept in case (2) contains same theID (causing msgs '*** insert: preserved ') *)
    2.52 -fun (*KEStore_Elems.*)add_thes th thes = (* for tests bypassing setup KEStore_Elems *)
    2.53 -  let
    2.54 -    fun add_the th ((thydata, theID)) =
    2.55 -      if can_insert theID th 
    2.56 -      then
    2.57 -        if exist_the theID th
    2.58 -        then (writeln ("*** insert: preserved " ^ strs2str theID); (fn x => x))
    2.59 -        else insrt theID thydata theID
    2.60 -      else
    2.61 -        let
    2.62 -          val th' = fill_parents th theID theID (*..*** insert: not found*)
    2.63 -          val th' = insrt theID thydata theID th'
    2.64 -        in merge_ptyps' th' end;
    2.65 -in fold (add_the th) thes end
    2.66 -
    2.67  fun Html_default exist = (Html {guh = theID2guh exist, 
    2.68    coursedesign = ["isac team 2006"], mathauthors = [], html = ""})
    2.69