1.1 --- a/src/Tools/isac/Interpret/appl.sml	Fri Oct 08 18:58:24 2010 +0200
     1.2 +++ b/src/Tools/isac/Interpret/appl.sml	Sat Oct 09 16:03:49 2010 +0200
     1.3 @@ -107,8 +107,7 @@
     1.4    in (bdv, pred) end
     1.5  
     1.6    | mk_set thy _ _ l _ = 
     1.7 -  error ("check_elementwise: no set "^
     1.8 -		 (Syntax.string_of_term (thy2ctxt thy) l));
     1.9 +    error ("check_elementwise: no set " ^ term2str l);
    1.10  (*> val consts = str2term "[x=#4]";
    1.11  > val pred = str2term "Assumptions";
    1.12  > val pt = union_asm pt p 
    1.13 @@ -116,7 +115,7 @@
    1.14     ("#0 <= x ^^^ #2 + #5 * x",[33]),("#0 <= #2 + x",[44])];
    1.15  > val p = [];
    1.16  > val (sss,ttt) = mk_set thy pt p consts pred;
    1.17 -> (Syntax.string_of_term (thy2ctxt thy) sss,Syntax.string_of_term(thy2ctxt thy) ttt);
    1.18 +> (term2str sss, term2str ttt);
    1.19  val it = ("x","((#0 <= sqrt x + sqrt (#5 + x) & #0 <= #9 + #4 * x) & ...
    1.20  
    1.21   val consts = str2term "UniversalList";