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