1.1 --- a/src/Tools/isac/calcelems.sml	Thu Sep 23 16:38:25 2010 +0200
     1.2 +++ b/src/Tools/isac/calcelems.sml	Sat Sep 25 16:49:33 2010 +0200
     1.3 @@ -606,10 +606,14 @@
     1.4    however, dynamic lookup is required, since "Isac" is not yet built here.*)
     1.5  fun term2str t = Print_Mode.setmp [] (Syntax.string_of_term
     1.6  (ProofContext.init_global (Thy_Info.get_theory "Isac"))) t;
     1.7 +fun terms2str ts = (strs2str o (map term2str )) ts;
     1.8 +(*terms2str [t1,t2] = "[\"1 + 2\",\"abc\"]";*)
     1.9 +fun terms2str' ts = (strs2str' o (map term2str )) ts;
    1.10 +(*terms2str' [t1,t2] = "[1 + 2,abc]";*)
    1.11 +fun terms2strs ts = (map term2str) ts;
    1.12 +(*terms2strs [t1,t2] = ["1 + 2", "abc"];*)
    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;
    1.17 +un type2str typ = Syntax.string_of_typ (thy2ctxt' "Isac") typ;
    1.18  val string_of_typ = type2str;
    1.19  
    1.20  fun subst2str (s:subst) =