1.1 --- a/test/Tools/isac/OLDTESTS/script_if.sml	Mon Jul 19 18:39:02 2021 +0200
     1.2 +++ b/test/Tools/isac/OLDTESTS/script_if.sml	Tue Jul 20 14:37:56 2021 +0200
     1.3 @@ -9,28 +9,28 @@
     1.4  (*---------------- 25.7.02 ---------------------*)
     1.5  
     1.6  val thy = (theory "Isac_Knowledge");
     1.7 -val t = (Thm.term_of o the o (TermC.parse thy)) "contains_root (sqrt(x)=1)";
     1.8 +val t = TermC.parseNEW'' thy "contains_root (sqrt(x)=1)";
     1.9  val SOME(ss,tt) = eval_contains_root "xxx" 1 t thy;
    1.10  
    1.11 -val t = (Thm.term_of o the o (TermC.parse thy)) "is_rootequation_in (sqrt(x)=1) x";
    1.12 +val t = TermC.parseNEW'' thy "is_rootequation_in (sqrt(x)=1) x";
    1.13  val SOME(ss,tt) = eval_is_rootequation_in "is_rootequation_i" 1 t thy; 
    1.14  
    1.15  (*---
    1.16 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
    1.17 -val t = (Thm.term_of o the o (TermC.parse thy)) "sqrt(#3+#4*x)";
    1.18 +val v = TermC.parseNEW'' thy "x";
    1.19 +val t = TermC.parseNEW'' thy "sqrt(#3+#4*x)";
    1.20  scan t v;
    1.21 -val t = (Thm.term_of o the o (TermC.parse thy)) "sqrt(#3+#4*a)";
    1.22 +val t = TermC.parseNEW'' thy "sqrt(#3+#4*a)";
    1.23  scan t v;
    1.24 -val t = (Thm.term_of o the o (TermC.parse thy)) "#1 + #2*sqrt(#3+#4*x)";
    1.25 +val t = TermC.parseNEW'' thy "#1 + #2*sqrt(#3+#4*x)";
    1.26  scan t v;
    1.27 -val t = (Thm.term_of o the o (TermC.parse thy)) "x + #2*sqrt(#3+#4*a)";
    1.28 +val t = TermC.parseNEW'' thy "x + #2*sqrt(#3+#4*a)";
    1.29  scan t v;
    1.30  ---*)
    1.31 -val t = (Thm.term_of o the o (TermC.parse thy)) 
    1.32 +val t = TermC.parseNEW'' thy 
    1.33  	    "is_rootequation_in (1 + 2*sqrt(3+4*x)=0) x";
    1.34  val SOME(ss,tt) = eval_is_rootequation_in "is_rootequation_i" 1 t thy; 
    1.35  
    1.36 -val t = (Thm.term_of o the o (TermC.parse thy)) 
    1.37 +val t = TermC.parseNEW'' thy 
    1.38  	    "is_rootequation_in (x + 2*sqrt(3+4*a)=0) x";
    1.39  val SOME(ss,tt) = eval_is_rootequation_in "is_rootequation_i" 1 t thy; 
    1.40