1.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml	Tue Jul 20 14:37:56 2021 +0200
     1.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml	Tue Jul 27 11:21:14 2021 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4  
     1.5  
     1.6  (*
     1.7 -> val t = TermC.parseNEW'' thy "#2 \<up> #3";
     1.8 +> val t = (Thm.term_of o the o (TermC.parse thy)) "#2 \<up> #3";
     1.9  > val eval_fn = the (LibraryC.assoc (!eval_list, "pow"));
    1.10  > val (SOME (id,t')) = get_pair thy "pow" eval_fn t;
    1.11  > Syntax.string_of_term (ThyC.to_ctxt thy) t';
    1.12 @@ -131,7 +131,7 @@
    1.13  " _________________ rewrite_ x+4_________________ ";
    1.14  " _________________ rewrite_ x+4_________________ ";
    1.15  " _________________ rewrite_ x+4_________________ ";
    1.16 -val t = TermC.parseNEW'' thy "sqrt(9+4*x)=sqrt x + sqrt(5+x)";
    1.17 +val t = (Thm.term_of o the o (TermC.parse thy)) "sqrt(9+4*x)=sqrt x + sqrt(5+x)";
    1.18  val thm = ThmC.numerals_to_Free @{thm square_equation_left};
    1.19  val (t,asm) = the (rewrite_ thy tless_true tval_rls true thm t);
    1.20  val rls = Test_simplify;
    1.21 @@ -374,7 +374,7 @@
    1.22  *)
    1.23  
    1.24  (*
    1.25 -val t = TermC.parseNEW'' thy "solutions (L::real set)";
    1.26 +val t = (Thm.term_of o the o (TermC.parse thy)) "solutions (L::real set)";
    1.27  TermC.atomty t;
    1.28  *)
    1.29