diff -r ce09935439b3 -r 2e0b7ca391dc test/Tools/isac/Knowledge/diophanteq.sml
--- a/test/Tools/isac/Knowledge/diophanteq.sml	Wed Aug 03 18:17:27 2022 +0200
+++ b/test/Tools/isac/Knowledge/diophanteq.sml	Thu Aug 04 12:48:37 2022 +0200
@@ -33,7 +33,7 @@
       SOME t' => t'
     | NONE => error "diophanteq.sml: syntax error in rewriting for usecase1";
 
-val SOME (t,_) = rewrite_inst_ ctxt e_rew_ord Rule_Set.empty true subst 
+val SOME (t,_) = rewrite_inst_ ctxt Rewrite_Ord.function_empty Rule_Set.empty true subst 
   @{thm "int_isolate_add"} t; UnparseC.term t;
 
 val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES"))) t;