1.1 --- a/src/Tools/isac/calcelems.sml	Thu Aug 19 15:41:56 2010 +0200
     1.2 +++ b/src/Tools/isac/calcelems.sml	Fri Aug 20 12:25:37 2010 +0200
     1.3 @@ -233,8 +233,6 @@
     1.4  type domID = string;   (* domID ^".thy" = theory' TODO.11.03replace by thyID*)
     1.5  type thyID = string;    (*WN.3.11.03 TODO: replace domID with thyID*)
     1.6  
     1.7 -(*2002 fun string_of_thy thy = 
     1.8 -((last_elem (Sign.stamp_names_of (sign_of thy)))^".thy"):theory';*)
     1.9  fun string_of_thy thy = Context.theory_name thy: theory';
    1.10  val theory2domID = string_of_thy;
    1.11  val theory2thyID = (get_thy o string_of_thy) : theory -> thyID;
    1.12 @@ -596,16 +594,12 @@
    1.13  	    else ass ids
    1.14      in ass (!calclist') : calcID end;
    1.15  
    1.16 -(*fun termopt2str (SOME t) = 
    1.17 -    "SOME " ^ (Sign.string_of_term (sign_of(assoc_thy "Isac.thy")) t)
    1.18 -  | termopt2str NONE = "NONE";*)
    1.19  fun termopt2str (SOME t) = 
    1.20      "SOME " ^ (Syntax.string_of_term (thy2ctxt' "Isac") t)
    1.21    | termopt2str NONE = "NONE";
    1.22  fun term2str t = Syntax.string_of_term (thy2ctxt' "Isac") t;
    1.23  fun terms2str ts= (strs2str o (map (Syntax.string_of_term 
    1.24  					(thy2ctxt' "Isac")))) ts;
    1.25 -(*fun type2str typ = Sign.string_of_typ (sign_of (assoc_thy "Isac.thy")) typ;*)
    1.26  fun type2str typ = Syntax.string_of_typ (thy2ctxt' "Isac") typ;
    1.27  val string_of_typ = type2str;
    1.28