1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Thu Aug 29 13:52:47 2019 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Tue Sep 03 12:40:27 2019 +0200
     1.3 @@ -558,7 +558,7 @@
     1.4  "--- does the predicate evaluate correctly ?";
     1.5  val t = str2term 
     1.6  	    "matchsub (?a * (?b - ?c)) (8 * (a - q) + a - 2 * q + 3 * (a - 2 * (q::real)))";
     1.7 -val ma = eval_matchsub "" "Tools.matchsub" t thy;
     1.8 +val ma = eval_matchsub "" "Prog_Expr.matchsub" t thy;
     1.9  case ma of
    1.10      SOME ("matchsub (?a * (?b - ?c)) (8 * (a - q) + \
    1.11  	  \a - 2 * q + 3 * (a - 2 * q)) = True", _) => ()
    1.12 @@ -567,7 +567,7 @@
    1.13  "--- does the respective prls rewrite ?";
    1.14  val prls = append_rls "prls_pbl_vereinf_poly" e_rls 
    1.15  	     [Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
    1.16 -	      Calc ("Tools.matchsub", eval_matchsub ""),
    1.17 +	      Calc ("Prog_Expr.matchsub", eval_matchsub ""),
    1.18  	      Thm ("or_true",@{thm or_true}),
    1.19  	      (*"(?a | True) = True"*)
    1.20  	      Thm ("or_false",@{thm or_false}),