diff -r ce09935439b3 -r 2e0b7ca391dc test/Tools/isac/Knowledge/polyeq-1.sml
--- a/test/Tools/isac/Knowledge/polyeq-1.sml	Wed Aug 03 18:17:27 2022 +0200
+++ b/test/Tools/isac/Knowledge/polyeq-1.sml	Thu Aug 04 12:48:37 2022 +0200
@@ -1018,31 +1018,31 @@
 then () else error "rls complete_square CHANGED";
 
 val thm = @{thm square_explicit1};
-val SOME (t,asm) = rewrite_ ctxt dummy_ord Rule_Set.Empty true thm t;
+val SOME (t,asm) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty true thm t;
 if UnparseC.term t = "(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - - 8"
 then () else error "thm square_explicit1 CHANGED";
 
 val thm = @{thm root_plus_minus};
-val SOME (t,asm) = rewrite_ ctxt dummy_ord PolyEq_erls true thm t;
+val SOME (t,asm) = rewrite_ ctxt Rewrite_Ord.function_empty PolyEq_erls true thm t;
 if UnparseC.term t =
 "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\n2 / 2 - x = - 1 * sqrt ((2 / 2) \<up> 2 - - 8)"
 then () else error "thm root_plus_minus CHANGED";
 
 (*the thm bdv_explicit2* here required to be constrained to ::real*)
 val thm = @{thm bdv_explicit2};
-val SOME (t,asm) = rewrite_inst_ ctxt dummy_ord Rule_Set.Empty true inst thm t;
+val SOME (t,asm) = rewrite_inst_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty true inst thm t;
 if UnparseC.term t =
 "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\n- 1 * x = - (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8)"
 then () else error "thm bdv_explicit2 CHANGED";
 
 val thm = @{thm bdv_explicit3};
-val SOME (t,asm) = rewrite_inst_ ctxt dummy_ord Rule_Set.Empty true inst thm t;
+val SOME (t,asm) = rewrite_inst_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty true inst thm t;
 if UnparseC.term t =
 "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8))"
 then () else error "thm bdv_explicit3 CHANGED";
 
 val thm = @{thm bdv_explicit2};
-val SOME (t,asm) = rewrite_inst_ ctxt dummy_ord Rule_Set.Empty true inst thm t;
+val SOME (t,asm) = rewrite_inst_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty true inst thm t;
 if UnparseC.term t =
 "- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - - 8) \<or>\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8))"
 then () else error "thm bdv_explicit2 CHANGED";