1.1 --- a/test/Tools/isac/Knowledge/polyeq-2.sml	Mon Apr 06 11:44:36 2020 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/polyeq-2.sml	Wed Apr 08 12:32:51 2020 +0200
     1.3 @@ -289,14 +289,14 @@
     1.4  t |> term2str; t |> atomty;
     1.5  val thm = num_str @{thm d2_prescind1};
     1.6  thm |> Thm.prop_of |> term2str; thm |> Thm.prop_of |> atomty;
     1.7 -val SOME (t', _) = rewrite_inst_ thy e_rew_ord e_rls true subst thm t; term2str t';
     1.8 +val SOME (t', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t; term2str t';
     1.9  
    1.10  (*x * (-6 + 5 * x) = 0   : Rewrite_Inst (["(''bdv'',x)"],("d2_reduce_equation1","")) 
    1.11                                                                          --> x = 0 | -6 + 5 * x = 0*)
    1.12  t' |> term2str; t' |> atomty;
    1.13  val thm = num_str @{thm d2_reduce_equation1};
    1.14  thm |> Thm.prop_of |> term2str; thm |> Thm.prop_of |> atomty;
    1.15 -val SOME (t'', _) = rewrite_inst_ thy e_rew_ord e_rls true subst thm t'; term2str t'';
    1.16 +val SOME (t'', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t'; term2str t'';
    1.17  (* NONE with d2_reduce_equation1:   "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))"
    1.18     instead   d2_reduce_equation1:   "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=(0::real)))"
    1.19  *)