diff -r 48c31909de24 -r 439f7f3867ec test/Tools/isac/MathEngBasic/rewrite.sml
--- a/test/Tools/isac/MathEngBasic/rewrite.sml	Wed Nov 16 10:30:59 2022 +0100
+++ b/test/Tools/isac/MathEngBasic/rewrite.sml	Wed Nov 16 17:42:41 2022 +0100
@@ -100,8 +100,8 @@
 val SOME (r, _) = (rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm tm);
 
 "----- ordered rewriting";
-fun tord (_:subst) pp = LibraryC.termless pp;
-if tord [] (@{term "x + y*z::real"}, @{term "y*z + x::real"}) then ()
+fun tord (_:Proof.context) (_:subst) pp = LibraryC.termless pp;
+if tord @{context} [] (@{term "x + y*z::real"}, @{term "y*z + x::real"}) then ()
 else error "rewrite.sml diff.behav. in ord.rewr.";
 
 val NONE = (rewrite_ ctxt tord Rule_Set.empty false thm tm);