test/Tools/isac/Knowledge/rateq.sml
changeset 60500 59a3af532717
parent 60424 c3acf9c442ac
child 60549 c0a775618258
     1.1 --- a/test/Tools/isac/Knowledge/rateq.sml	Thu Jul 28 11:43:27 2022 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/rateq.sml	Sat Jul 30 16:47:45 2022 +0200
     1.3 @@ -21,22 +21,22 @@
     1.4  "------------ pbl: rational, univariate, equation ----------------";
     1.5  "------------ pbl: rational, univariate, equation ----------------";
     1.6  val t = TermC.parseNEW' ctxt "(1/b+1/x=1) is_ratequation_in  x";
     1.7 -val SOME (t_, _) = rewrite_set_ thy  false RatEq_prls t;
     1.8 +val SOME (t_, _) = rewrite_set_ ctxt  false RatEq_prls t;
     1.9  val result = UnparseC.term t_;
    1.10  if result <>  "True"  then error "rateq.sml: new behaviour 1:" else ();
    1.11  
    1.12  val t = TermC.parseNEW' ctxt "(sqrt(x)=1) is_ratequation_in  x";
    1.13 -val SOME (t_, _) = rewrite_set_ thy  false RatEq_prls t;
    1.14 +val SOME (t_, _) = rewrite_set_ ctxt  false RatEq_prls t;
    1.15  val result = UnparseC.term t_;
    1.16  if result <>  "False"  then error "rateq.sml: new behaviour 2:" else ();
    1.17  
    1.18  val t = TermC.parseNEW' ctxt "(x=- 1) is_ratequation_in x";
    1.19 -val SOME (t_,_) = rewrite_set_ thy  false RatEq_prls t;
    1.20 +val SOME (t_,_) = rewrite_set_ ctxt  false RatEq_prls t;
    1.21  val result = UnparseC.term t_;
    1.22  if result <>  "False"  then error "rateq.sml: new behaviour 3:" else ();
    1.23  
    1.24  val t = TermC.parseNEW' ctxt "(3 + x \<up> 2 + 1/(x \<up> 2+3)=1) is_ratequation_in x";
    1.25 -val SOME (t_,_) = rewrite_set_ thy  false RatEq_prls t;
    1.26 +val SOME (t_,_) = rewrite_set_ ctxt  false RatEq_prls t;
    1.27  val result = UnparseC.term t_;
    1.28  if result <>  "True"  then error "rateq.sml: new behaviour 4:" else ();
    1.29