1.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml	Thu Apr 09 12:03:14 2020 +0200
     1.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml	Thu Apr 09 17:13:17 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' = term2str t;
     1.8 +val t' = UnparseC.term2str 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 @@ -262,7 +262,7 @@
    1.13  			 ["sqroot-test","univariate","equation","test"]);
    1.14  val loc = Istate.empty;
    1.15  val (pt,pos) = (e_ctree,[]);
    1.16 -val (pt,_) = cappend_problem pt pos loc e_fmz (oris,empty_spec,e_term, ContextC.empty)
    1.17 +val (pt,_) = cappend_problem pt pos loc e_fmz (oris,empty_spec,TermC.empty, ContextC.empty)
    1.18  val pt = update_branch pt [] TransitiveB;
    1.19  (*
    1.20  val pt = update_model pt [] (map init_item (snd (get_obj g_origin pt [])));
    1.21 @@ -297,7 +297,7 @@
    1.22  
    1.23  val pos = (lev_on o lev_dn) pos;
    1.24  val thm = ("square_equation_left",""); val ctold = ct;
    1.25 -val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") true thm (term2str ct));
    1.26 +val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") true thm (UnparseC.term2str ct));
    1.27  val (pt,_) = cappend_atomic pt pos loc ctold (Tac (fst thm)) (str2term ct,[])Complete;
    1.28  (*val pt = union_asm pt [] (map (rpair []) asm);*)
    1.29  
    1.30 @@ -545,7 +545,7 @@
    1.31  (*.9.6.03
    1.32   val t = str2term "sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)";
    1.33   val SOME (t',asm) = rewrite_set_ thy false rls t;
    1.34 - term2str t';
    1.35 + UnparseC.term2str t';
    1.36  > trace_rewrite:=true; 
    1.37   trace_rewrite:=false; 
    1.38  *)
    1.39 @@ -630,6 +630,6 @@
    1.40  else ();
    1.41  
    1.42  writeln (pr_ctree pr_short pt);
    1.43 -writeln("result: "^((term2str o fst o (get_obj g_result pt)) [])^
    1.44 +writeln("result: "^((UnparseC.term2str o fst o (get_obj g_result pt)) [])^
    1.45  "\n==============================================================");
    1.46