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