1.1 --- a/src/Tools/isac/calcelems.sml	Fri Oct 08 18:58:24 2010 +0200
     1.2 +++ b/src/Tools/isac/calcelems.sml	Sat Oct 09 16:03:49 2010 +0200
     1.3 @@ -5,10 +5,9 @@
     1.4     they are defined here at the beginning of the code.
     1.5     author: Walther Neuper
     1.6     (c) isac-team 2003
     1.7 - 
     1.8 -use"calcelems.sml";
     1.9  *)
    1.10  
    1.11 +
    1.12  val linefeed = (curry op^) "\n";
    1.13  type authors = string list;
    1.14  
    1.15 @@ -596,12 +595,6 @@
    1.16  	    else ass ids
    1.17      in ass (!calclist') : calcID end;
    1.18  
    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; Isa2002*)
    1.23 -(*Florian1009: 'val' would ensure static lookup, i.e. only at compile time;
    1.24 -  however, dynamic lookup is required, since "Isac" is not yet built here.*)
    1.25  fun term2str t = Print_Mode.setmp [] (Syntax.string_of_term
    1.26  (ProofContext.init_global (Thy_Info.get_theory "Isac"))) t;
    1.27  
    1.28 @@ -612,7 +605,11 @@
    1.29  fun terms2strs ts = (map term2str) ts;
    1.30  (*terms2strs [t1,t2] = ["1 + 2", "abc"];*)
    1.31  
    1.32 -fun type2str typ = Syntax.string_of_typ (thy2ctxt' "Isac") typ;
    1.33 +fun termopt2str (SOME t) = "SOME " ^ term2str t
    1.34 +  | termopt2str NONE = "NONE";
    1.35 +
    1.36 +fun type2str typ = 
    1.37 +    Print_Mode.setmp [] (Syntax.string_of_typ (thy2ctxt' "Isac")) typ;
    1.38  val string_of_typ = type2str;
    1.39  
    1.40  fun subst2str (s:subst) =