1.1 --- a/src/Tools/isac/calcelems.sml	Fri Jun 06 07:10:26 2014 +0200
     1.2 +++ b/src/Tools/isac/calcelems.sml	Fri Jun 06 14:49:18 2014 +0200
     1.3 @@ -476,6 +476,12 @@
     1.4  			    mathauthors: authors,
     1.5  			    ord: (subst -> (term * term) -> bool)};
     1.6  val e_thydata = Html {guh="e_guh", coursedesign=[], mathauthors=[], html=""};
     1.7 +fun the2str (Html {guh, coursedesign, mathauthors, html}) = guh : string
     1.8 +  | the2str (Hthm {guh, coursedesign, mathauthors, fillpats, thm}) = guh
     1.9 +  | the2str (Hrls {guh, coursedesign, mathauthors, thy_rls}) = guh
    1.10 +  | the2str (Hcal {guh, coursedesign, mathauthors, calc}) = guh
    1.11 +  | the2str (Hord {guh, coursedesign, mathauthors, ord}) = guh
    1.12 +fun thes2str thes = map the2str thes |> list2str;
    1.13  
    1.14  type thehier = (thydata ptyp) list;
    1.15  (* required to determine sequence of main nodes of thehier in KEStore.thy *)