1.1 --- a/test/Tools/isac/OLDTESTS/script_if.sml	Mon Dec 07 11:32:12 2015 +0100
     1.2 +++ b/test/Tools/isac/OLDTESTS/script_if.sml	Mon Dec 07 14:10:59 2015 +0100
     1.3 @@ -9,35 +9,35 @@
     1.4  (*---------------- 25.7.02 ---------------------*)
     1.5  
     1.6  val thy = (theory "Isac");
     1.7 -val t = (term_of o the o (parse thy)) "contains_root (sqrt(x)=1)";
     1.8 +val t = (Thm.term_of o the o (parse 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 = (term_of o the o (parse thy)) "is_rootequation_in (sqrt(x)=1) x";
    1.12 +val t = (Thm.term_of o the o (parse 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 = (term_of o the o (parse thy)) "x";
    1.17 -val t = (term_of o the o (parse thy)) "sqrt(#3+#4*x)";
    1.18 +val v = (Thm.term_of o the o (parse thy)) "x";
    1.19 +val t = (Thm.term_of o the o (parse thy)) "sqrt(#3+#4*x)";
    1.20  scan t v;
    1.21 -val t = (term_of o the o (parse thy)) "sqrt(#3+#4*a)";
    1.22 +val t = (Thm.term_of o the o (parse thy)) "sqrt(#3+#4*a)";
    1.23  scan t v;
    1.24 -val t = (term_of o the o (parse thy)) "#1 + #2*sqrt(#3+#4*x)";
    1.25 +val t = (Thm.term_of o the o (parse thy)) "#1 + #2*sqrt(#3+#4*x)";
    1.26  scan t v;
    1.27 -val t = (term_of o the o (parse thy)) "x + #2*sqrt(#3+#4*a)";
    1.28 +val t = (Thm.term_of o the o (parse thy)) "x + #2*sqrt(#3+#4*a)";
    1.29  scan t v;
    1.30  ---*)
    1.31 -val t = (term_of o the o (parse thy)) 
    1.32 +val t = (Thm.term_of o the o (parse 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 = (term_of o the o (parse thy)) 
    1.37 +val t = (Thm.term_of o the o (parse 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  
    1.41 -val t = (term_of o the o (parse Test.thy)) 
    1.42 +val t = (Thm.term_of o the o (parse Test.thy)) 
    1.43  	    "is_rootequation_in (sqrt(x)=1) x";
    1.44  atomty t;
    1.45 -val t = (term_of o the o (parse (theory "Isac"))) 
    1.46 +val t = (Thm.term_of o the o (parse (theory "Isac"))) 
    1.47  	    "is_rootequation_in (sqrt(x)=1) x";
    1.48  atomty t;
    1.49