# HG changeset patch
# User Walther Neuper <neuper@ist.tugraz.at>
# Date 1403157100 -7200
# Node ID 1395832f4f53662492e82b94e6ba2ae7861fca9b
# Parent  a7c61c0bd4379934bad06af4f954e63deff9d0da
ad 967c8a1eb6b1 (7) thehier: remove code superfluous by last changeset

diff -r a7c61c0bd437 -r 1395832f4f53 src/Tools/isac/Interpret/rewtools.sml
--- a/src/Tools/isac/Interpret/rewtools.sml	Thu Jun 19 07:40:46 2014 +0200
+++ b/src/Tools/isac/Interpret/rewtools.sml	Thu Jun 19 07:51:40 2014 +0200
@@ -653,28 +653,6 @@
     (tracing ("### atomic_appl_tacs: not impl. for tac = '"^ tac2str tac ^"'");
      []);
 
-
-
-
-
-(*.not only for thydata, but also for thy's etc.*)
-fun theID2guh (theID:theID) =
-    case length theID of
-	0 => error ("theID2guh: called with theID = "^strs2str' theID)
-      | 1 => part2guh theID
-      | 2 => thy2guh theID
-      | 3 => thypart2guh theID
-      | 4 => let val [isa, thyID, typ, elemID] = theID
-	     in case typ of
-		    "Theorems" => thm2guh (isa, thyID) elemID
-		  | "Rulesets" => rls2guh (isa, thyID) elemID
-		  | "Calculations" => cal2guh (isa, thyID) elemID
-		  | "Orders" => ord2guh (isa, thyID) elemID
-		  | "Theorems" => thy2guh [isa, thyID]
-		  | str => error ("theID2guh: called with theID = "^
-					strs2str' theID)
-	     end
-      | n => error ("theID2guh called with theID = "^strs2str' theID);
 (*.filenames not only for thydata, but also for thy's etc.*)
 fun theID2filename (theID:theID) = theID2guh theID ^ ".xml" : filename;
 
diff -r a7c61c0bd437 -r 1395832f4f53 src/Tools/isac/calcelems.sml
--- a/src/Tools/isac/calcelems.sml	Thu Jun 19 07:40:46 2014 +0200
+++ b/src/Tools/isac/calcelems.sml	Thu Jun 19 07:51:40 2014 +0200
@@ -975,66 +975,6 @@
 		      "consider setting 'check_guhs_unique := false'")
     else ();
 
-(* for preserving elements created by 'fun store_thy' *)
-fun exist_the (theID : theID) (thy_hie : thehier) =
-  let 
-    fun node theID ids (Ptyp (id, _, ns)) =
-      if theID = ids @ [id] then true else nodes theID (ids @ [id]) ns
-    and nodes _ _ [] = false
-      | nodes theID ids (n::ns) =
-        if node theID ids n then true else nodes theID ids ns
-  in nodes theID [] thy_hie end;
-
-(* insrt requires a parent; see 'fun fill_parents' *)
-fun can_insert (theID : theID) (thy_hie : thehier) = 
-  (insrt theID e_thydata theID thy_hie; true)
-    handle _ => false;
-    
-(* cut 'theID', the ID of theory elements from tail to head
-   until insertion into the hierarchy of theory elements 'th' is possible
-   (the hierarchy requires the parentnode to exist for insertion) *)
-fun cut_theID th ([] : theID) = error "could not insert into thy-hierarchy"
-  | cut_theID th theID  = 
-    if can_insert theID th
-    then theID else cut_theID th (drop_last theID);
-
-(* insert empty parents 'Html' into the hierarchy of theory elements 'th'
-   until the actual node can be inserted with key 'theID' *)
-fun fill_parents th cutID theID =
-  let val cutID' = cut_theID th cutID
-  in if cutID' = theID
-    then th
-    else 
-      let 
-        val th' = insrt cutID' (Html {guh=theID2guh theID, coursedesign = ["isac team 2006"],
-          mathauthors = [], html = ""}) cutID' th
-        val cutID_ = cutID' @ [nth ((length cutID') + 1) theID]
-      in fill_parents th' cutID_ theID end
-  end;
-
-(* argument 1 "th : thehier": contains some thydata from "setup {* KEStore_Elems.add_thes ..."
-   argument 1 "th : thehier": contains some thydata from "store_thes ..."
-      already in some "ProgLang/*.thy" or "Knowledge/*.thy"
-   argument 2 "(theID, thydata)::_ : (theID * thydata) list: contains thydata collected
-      automatically in Build_Thydata.thy finally.
-   parents of thydata in list, missing in thehier, are inserted 
-      (causing msgs '*** insert: not found');
-   (1) is kept in case (2) contains same theID (causing msgs '*** insert: preserved ') *)
-fun (*KEStore_Elems.*)add_thes th thes = (* for tests bypassing setup KEStore_Elems *)
-  let
-    fun add_the th ((thydata, theID)) =
-      if can_insert theID th 
-      then
-        if exist_the theID th
-        then (writeln ("*** insert: preserved " ^ strs2str theID); (fn x => x))
-        else insrt theID thydata theID
-      else
-        let
-          val th' = fill_parents th theID theID (*..*** insert: not found*)
-          val th' = insrt theID thydata theID th'
-        in merge_ptyps' th' end;
-in fold (add_the th) thes end
-
 fun Html_default exist = (Html {guh = theID2guh exist, 
   coursedesign = ["isac team 2006"], mathauthors = [], html = ""})