diff -r 137227934d2e -r 145e45cd7a0f src/Tools/isac/MathEngBasic/tactic.sml
--- a/src/Tools/isac/MathEngBasic/tactic.sml	Wed Aug 03 13:22:36 2022 +0200
+++ b/src/Tools/isac/MathEngBasic/tactic.sml	Wed Aug 03 17:18:47 2022 +0200
@@ -271,9 +271,10 @@
     try_rew ctxt Rewrite_Ord.e_rew_ordX Rule_Set.empty [] f 
       (Rule.Eval (assoc_calc' (Proof_Context.theory_of ctxt) scrID |> snd))
   | applicable ctxt ro erls f (Rewrite thm'') =
-    try_rew ctxt (ro, Rewrite_Ord.assoc_rew_ord ro) erls [] f (Rule.Thm thm'')
+    try_rew ctxt (ro, assoc_rew_ord (Proof_Context.theory_of ctxt) ro) erls [] f (Rule.Thm thm'')
   | applicable ctxt ro erls f (Rewrite_Inst (subs, thm'')) =
-    try_rew ctxt (ro, Rewrite_Ord.assoc_rew_ord ro) erls (Subst.T_from_input ctxt subs) f (Rule.Thm thm'')
+    try_rew ctxt (ro, assoc_rew_ord (Proof_Context.theory_of ctxt) ro) erls 
+      (Subst.T_from_input ctxt subs) f (Rule.Thm thm'')
 
   | applicable thy _ _ f (Rewrite_Set rls') =
     filter_appl_rews thy [] f (assoc_rls rls')