diff -r ce09935439b3 -r 2e0b7ca391dc test/Tools/isac/Knowledge/polyeq-2.sml
--- a/test/Tools/isac/Knowledge/polyeq-2.sml	Wed Aug 03 18:17:27 2022 +0200
+++ b/test/Tools/isac/Knowledge/polyeq-2.sml	Thu Aug 04 12:48:37 2022 +0200
@@ -287,14 +287,14 @@
 t |> UnparseC.term; t |> TermC.atomty;
 val thm = @{thm d2_prescind1};
 thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atomty;
-val SOME (t', _) = rewrite_inst_ ctxt e_rew_ord Rule_Set.empty true subst thm t; UnparseC.term t';
+val SOME (t', _) = rewrite_inst_ ctxt Rewrite_Ord.function_empty Rule_Set.empty true subst thm t; UnparseC.term t';
 
 (*x * (-6 + 5 * x) = 0   : Rewrite_Inst (["(''bdv'',x)"],("d2_reduce_equation1", "")) 
                                                                         --> x = 0 | -6 + 5 * x = 0*)
 t' |> UnparseC.term; t' |> TermC.atomty;
 val thm = @{thm d2_reduce_equation1};
 thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atomty;
-val SOME (t'', _) = rewrite_inst_ ctxt e_rew_ord Rule_Set.empty true subst thm t'; UnparseC.term t'';
+val SOME (t'', _) = rewrite_inst_ ctxt Rewrite_Ord.function_empty Rule_Set.empty true subst thm t'; UnparseC.term t'';
 (* NONE with d2_reduce_equation1:   "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))"
    instead   d2_reduce_equation1:   "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=(0::real)))"
 *)