1.1 --- a/test/Tools/isac/Knowledge/rateq.sml	Mon Apr 19 11:45:43 2021 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/rateq.sml	Mon Apr 19 15:02:00 2021 +0200
     1.3 @@ -20,22 +20,22 @@
     1.4  "------------ pbl: rational, univariate, equation ----------------";
     1.5  "------------ pbl: rational, univariate, equation ----------------";
     1.6  "------------ pbl: rational, univariate, equation ----------------";
     1.7 -val t = (Thm.term_of o the o (parse thy)) "(1/b+1/x=1) is_ratequation_in  x";
     1.8 +val t = (Thm.term_of o the o (TermC.parse thy)) "(1/b+1/x=1) is_ratequation_in  x";
     1.9  val SOME (t_, _) = rewrite_set_ thy  false RatEq_prls t;
    1.10  val result = UnparseC.term t_;
    1.11  if result <>  "True"  then error "rateq.sml: new behaviour 1:" else ();
    1.12  
    1.13 -val t = (Thm.term_of o the o (parse thy)) "(sqrt(x)=1) is_ratequation_in  x";
    1.14 +val t = (Thm.term_of o the o (TermC.parse thy)) "(sqrt(x)=1) is_ratequation_in  x";
    1.15  val SOME (t_, _) = rewrite_set_ thy  false RatEq_prls t;
    1.16  val result = UnparseC.term t_;
    1.17  if result <>  "False"  then error "rateq.sml: new behaviour 2:" else ();
    1.18  
    1.19 -val t = (Thm.term_of o the o (parse thy)) "(x=-1) is_ratequation_in x";
    1.20 +val t = (Thm.term_of o the o (TermC.parse thy)) "(x=-1) is_ratequation_in x";
    1.21  val SOME (t_,_) = rewrite_set_ thy  false RatEq_prls t;
    1.22  val result = UnparseC.term t_;
    1.23  if result <>  "False"  then error "rateq.sml: new behaviour 3:" else ();
    1.24  
    1.25 -val t = (Thm.term_of o the o (parse thy)) "(3 + x^^^2 + 1/(x^^^2+3)=1) is_ratequation_in x";
    1.26 +val t = (Thm.term_of o the o (TermC.parse thy)) "(3 + x^^^2 + 1/(x^^^2+3)=1) is_ratequation_in x";
    1.27  val SOME (t_,_) = rewrite_set_ thy  false RatEq_prls t;
    1.28  val result = UnparseC.term t_;
    1.29  if result <>  "True"  then error "rateq.sml: new behaviour 4:" else ();
    1.30 @@ -148,7 +148,7 @@
    1.31  
    1.32  UnparseC.term bdv = "x";
    1.33  UnparseC.terms asms = (* asms from rewriting are missing : vvv *)
    1.34 -  ("[\"<not> matches (?a = 0) (1 = 5 * x) | ~ lhs (1 = 5 * x) is_poly_in x\",\"x = 1 / 5\", " ^
    1.35 +  ("[\"<not> TermC.matches (?a = 0) (1 = 5 * x) | ~ lhs (1 = 5 * x) is_poly_in x\",\"x = 1 / 5\", " ^
    1.36     "\"lhs (1 + -5 * x = 0) is_poly_in x\",\"lhs (1 + -5 * x = 0) has_degree_in x = 1\", " ^
    1.37     "\"1 / x = 5 is_ratequation_in x\"]");
    1.38  (*
    1.39 @@ -158,7 +158,7 @@
    1.40  val Applicable.Yes (Check_elementwise' (curr_form, pred, (res, asms))) = check p''''' pt''''' m''''';
    1.41  UnparseC.term curr_form = "[x = 1 / 5]";
    1.42  pred = "Assumptions";
    1.43 -res = str2term "[]::bool list";
    1.44 +res = TermC.str2term "[]::bool list";
    1.45  asms = [];
    1.46  
    1.47  val (p,_,f,nxt,_,pt) = me nxt''' p''' [] pt'''; (*<<<----- this caused the error*)
    1.48 @@ -286,7 +286,7 @@
    1.49  
    1.50  (*     *)if eq_set op = ((Ctree.get_assumptions pt p |> map UnparseC.term), [
    1.51  (*0.pre*)  "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x",
    1.52 -(*1.pre*)  "\<not> matches (?a = 0)\n        ((3 + -1 * x + x ^^^ 2) * x =\n         1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) \<or>\n"
    1.53 +(*1.pre*)  "\<not> TermC.matches (?a = 0)\n        ((3 + -1 * x + x ^^^ 2) * x =\n         1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) \<or>\n"
    1.54  (*1.pre*)    ^ "\<not> lhs ((3 + -1 * x + x ^^^ 2) * x =\n            1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x",
    1.55  (*2.pre*)  "lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x", 
    1.56  (*2.pre*)  "lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2",
    1.57 @@ -308,7 +308,7 @@
    1.58  if f2str f = "[x = 6 / 5]" andalso eq_set op = (map UnparseC.term (Ctree.get_assumptions pt p),
    1.59   ["x = 6 / 5", "lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x",
    1.60    "lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2",
    1.61 -  "\<not> matches (?a = 0)\n        ((3 + -1 * x + x ^^^ 2) * x =\n         1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) \<or>\n\<not> lhs ((3 + -1 * x + x ^^^ 2) * x =\n            1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x",
    1.62 +  "\<not> TermC.matches (?a = 0)\n        ((3 + -1 * x + x ^^^ 2) * x =\n         1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) \<or>\n\<not> lhs ((3 + -1 * x + x ^^^ 2) * x =\n            1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x",
    1.63    "x \<noteq> 0", "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0",
    1.64    "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x"])
    1.65  then () else error "test CHANGED";