1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Wed Apr 15 11:11:54 2020 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Wed Apr 15 11:37:43 2020 +0200
     1.3 @@ -567,8 +567,8 @@
     1.4  
     1.5  "--- does the respective prls rewrite ?";
     1.6  val prls = Rule_Set.append_rules "prls_pbl_vereinf_poly" Rule_Set.empty 
     1.7 -	     [Num_Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
     1.8 -	      Num_Calc ("Prog_Expr.matchsub", eval_matchsub ""),
     1.9 +	     [Eval ("Poly.is'_polyexp", eval_is_polyexp ""),
    1.10 +	      Eval ("Prog_Expr.matchsub", eval_matchsub ""),
    1.11  	      Thm ("or_true",@{thm or_true}),
    1.12  	      (*"(?a | True) = True"*)
    1.13  	      Thm ("or_false",@{thm or_false}),