1.1 --- a/src/Tools/isac/calcelems.sml	Wed Mar 12 17:43:22 2014 +0100
     1.2 +++ b/src/Tools/isac/calcelems.sml	Mon Mar 17 08:54:48 2014 +0100
     1.3 @@ -485,6 +485,14 @@
     1.4  
     1.5  type thehier = (thydata ptyp) list;
     1.6  val thehier = Unsynchronized.ref ([] : thehier); (*WN101011 make argument, del*)
     1.7 +(* required to determine sequence of main nodes of thehier in KEStore.thy *)
     1.8 +fun part2guh ([str]:theID) =
     1.9 +    (case str of
    1.10 +	"Isabelle" => "thy_isab_" ^ str ^ "-part" : guh
    1.11 +      | "IsacScripts" => "thy_scri_" ^ str ^ "-part"
    1.12 +      | "IsacKnowledge" => "thy_isac_" ^ str ^ "-part"
    1.13 +      | str => error ("thy2guh: called with '"^str^"'"))
    1.14 +  | part2guh theID = error ("part2guh called with theID = " ^ theID2str theID);
    1.15  
    1.16  (* an association list, gets the value once in Isac.ML.
    1.17     stores Isabelle's thms as terms for compatibility with Theory.axioms_of.