1.1 --- a/src/Tools/isac/calcelems.sml	Thu Sep 23 08:54:26 2010 +0200
     1.2 +++ b/src/Tools/isac/calcelems.sml	Thu Sep 23 12:56:51 2010 +0200
     1.3 @@ -601,7 +601,12 @@
     1.4  fun termopt2str (SOME t) = 
     1.5      "SOME " ^ (Syntax.string_of_term (thy2ctxt' "Isac") t)
     1.6    | termopt2str NONE = "NONE";
     1.7 -fun term2str t = Syntax.string_of_term (thy2ctxt' "Isac") t;
     1.8 +(*fun term2str t = Syntax.string_of_term (thy2ctxt' "Isac") t; Isa2002*)
     1.9 +(*Florian1009: 'val' would ensure static lookup, i.e. only at compile time;
    1.10 +  however, dynamic lookup is required, since "Isac" is not yet built here.*)
    1.11 +fun term2str t = Print_Mode.setmp [] (Syntax.string_of_term
    1.12 +(ProofContext.init_global (Thy_Info.get_theory "Isac"))) t;
    1.13 +
    1.14  fun terms2str ts= (strs2str o (map (Syntax.string_of_term 
    1.15  					(thy2ctxt' "Isac")))) ts;
    1.16  fun type2str typ = Syntax.string_of_typ (thy2ctxt' "Isac") typ;