1.1 --- a/test/Tools/isac/OLDTESTS/script_if.sml	Mon Apr 19 11:45:43 2021 +0200
     1.2 +++ b/test/Tools/isac/OLDTESTS/script_if.sml	Mon Apr 19 15:02:00 2021 +0200
     1.3 @@ -9,37 +9,37 @@
     1.4  (*---------------- 25.7.02 ---------------------*)
     1.5  
     1.6  val thy = (theory "Isac_Knowledge");
     1.7 -val t = (Thm.term_of o the o (parse thy)) "contains_root (sqrt(x)=1)";
     1.8 +val t = (Thm.term_of o the o (TermC.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 = (Thm.term_of o the o (parse thy)) "is_rootequation_in (sqrt(x)=1) x";
    1.12 +val t = (Thm.term_of o the o (TermC.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 = (Thm.term_of o the o (parse thy)) "x";
    1.17 -val t = (Thm.term_of o the o (parse thy)) "sqrt(#3+#4*x)";
    1.18 +val v = (Thm.term_of o the o (TermC.parse thy)) "x";
    1.19 +val t = (Thm.term_of o the o (TermC.parse thy)) "sqrt(#3+#4*x)";
    1.20  scan t v;
    1.21 -val t = (Thm.term_of o the o (parse thy)) "sqrt(#3+#4*a)";
    1.22 +val t = (Thm.term_of o the o (TermC.parse thy)) "sqrt(#3+#4*a)";
    1.23  scan t v;
    1.24 -val t = (Thm.term_of o the o (parse thy)) "#1 + #2*sqrt(#3+#4*x)";
    1.25 +val t = (Thm.term_of o the o (TermC.parse thy)) "#1 + #2*sqrt(#3+#4*x)";
    1.26  scan t v;
    1.27 -val t = (Thm.term_of o the o (parse thy)) "x + #2*sqrt(#3+#4*a)";
    1.28 +val t = (Thm.term_of o the o (TermC.parse thy)) "x + #2*sqrt(#3+#4*a)";
    1.29  scan t v;
    1.30  ---*)
    1.31 -val t = (Thm.term_of o the o (parse thy)) 
    1.32 +val t = (Thm.term_of o the o (TermC.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 = (Thm.term_of o the o (parse thy)) 
    1.37 +val t = (Thm.term_of o the o (TermC.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 = (Thm.term_of o the o (parse Test.thy)) 
    1.42 +val t = (Thm.term_of o the o (TermC.parse Test.thy)) 
    1.43  	    "is_rootequation_in (sqrt(x)=1) x";
    1.44 -atomty t;
    1.45 -val t = (Thm.term_of o the o (parse (theory "Isac_Knowledge"))) 
    1.46 +TermC.atomty t;
    1.47 +val t = (Thm.term_of o the o (TermC.parse (theory "Isac_Knowledge"))) 
    1.48  	    "is_rootequation_in (sqrt(x)=1) x";
    1.49 -atomty t;
    1.50 +TermC.atomty t;
    1.51  
    1.52  (*
    1.53  val SOME(tt,_) = rewrite_set_ Test.thytrue tval_rls t;
    1.54 @@ -71,9 +71,9 @@
    1.55    [Problem.prep_input (theory "Isac_Knowledge")
    1.56        (["approximate", "univariate", "equation", "test"],
    1.57          [("#Given", ["equality e_e", "solveFor v_v", "errorBound err_"]),
    1.58 -          ("#Where", ["matches (?a = ?b) e_e"]),
    1.59 +          ("#Where", ["TermC.matches (?a = ?b) e_e"]),
    1.60            ("#Find", ["solutions v_i_"])],
    1.61 -        Rule_Set.append_rules Rule_Set.empty [Eval ("Prog_Expr.matches",eval_matches "#matches_")], [])]
    1.62 +        Rule_Set.append_rules Rule_Set.empty [Eval ("Prog_Expr.TermC.matches",eval_matches "#matches_")], [])]
    1.63    thy;
    1.64  
    1.65  methods:= overwritel (!methods,