1.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml	Fri Apr 10 16:16:09 2020 +0200
     1.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml	Fri Apr 10 18:32:36 2020 +0200
     1.3 @@ -198,7 +198,7 @@
     1.4  val (t,_) = the (rewrite_set_inst_ thy false subst rls t);
     1.5  val rls = Test_simplify;
     1.6  val (t,_) = the (rewrite_set_ thy false rls t);
     1.7 -val t' = UnparseC.term2str t;
     1.8 +val t' = UnparseC.term t;
     1.9  if t' = "x = 4" then ()
    1.10  else error "root-equ.sml: new behav. in rewrite_ x+4";
    1.11  
    1.12 @@ -297,7 +297,7 @@
    1.13  
    1.14  val pos = (lev_on o lev_dn) pos;
    1.15  val thm = ("square_equation_left",""); val ctold = ct;
    1.16 -val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") true thm (UnparseC.term2str ct));
    1.17 +val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") true thm (UnparseC.term ct));
    1.18  val (pt,_) = cappend_atomic pt pos loc ctold (Tac (fst thm)) (str2term ct,[])Complete;
    1.19  (*val pt = union_asm pt [] (map (rpair []) asm);*)
    1.20  
    1.21 @@ -545,7 +545,7 @@
    1.22  (*.9.6.03
    1.23   val t = str2term "sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)";
    1.24   val SOME (t',asm) = rewrite_set_ thy false rls t;
    1.25 - UnparseC.term2str t';
    1.26 + UnparseC.term t';
    1.27  > trace_rewrite:=true; 
    1.28   trace_rewrite:=false; 
    1.29  *)
    1.30 @@ -630,6 +630,6 @@
    1.31  else ();
    1.32  
    1.33  writeln (pr_ctree pr_short pt);
    1.34 -writeln("result: "^((UnparseC.term2str o fst o (get_obj g_result pt)) [])^
    1.35 +writeln("result: "^((UnparseC.term o fst o (get_obj g_result pt)) [])^
    1.36  "\n==============================================================");
    1.37