1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Fri Jan 17 12:37:21 2020 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Fri Jan 17 13:14:11 2020 +0100
     1.3 @@ -567,8 +567,8 @@
     1.4  
     1.5  "--- does the respective prls rewrite ?";
     1.6  val prls = append_rls "prls_pbl_vereinf_poly" e_rls 
     1.7 -	     [Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
     1.8 -	      Calc ("Prog_Expr.matchsub", eval_matchsub ""),
     1.9 +	     [Num_Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
    1.10 +	      Num_Calc ("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}),