1.1 --- a/test/Tools/isac/Knowledge/rateq.sml	Mon Dec 07 11:32:12 2015 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/rateq.sml	Mon Dec 07 14:10:59 2015 +0100
     1.3 @@ -19,22 +19,22 @@
     1.4  "------------ pbl: rational, univariate, equation ----------------";
     1.5  "------------ pbl: rational, univariate, equation ----------------";
     1.6  "------------ pbl: rational, univariate, equation ----------------";
     1.7 -val t = (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 (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 = term2str t_;
    1.11  if result <>  "True"  then error "rateq.sml: new behaviour 1:" else ();
    1.12  
    1.13 -val t = (term_of o the o (parse thy)) "(sqrt(x)=1) is_ratequation_in  x";
    1.14 +val t = (Thm.term_of o the o (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 = term2str t_;
    1.17  if result <>  "False"  then error "rateq.sml: new behaviour 2:" else ();
    1.18  
    1.19 -val t = (term_of o the o (parse thy)) "(x=-1) is_ratequation_in x";
    1.20 +val t = (Thm.term_of o the o (parse thy)) "(x=-1) is_ratequation_in x";
    1.21  val SOME (t_,_) = rewrite_set_ thy  false RatEq_prls t;
    1.22  val result = term2str t_;
    1.23  if result <>  "False"  then error "rateq.sml: new behaviour 3:" else ();
    1.24  
    1.25 -val t = (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 (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 = term2str t_;
    1.29  if result <>  "True"  then error "rateq.sml: new behaviour 4:" else ();