1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml	Wed Aug 03 13:22:36 2022 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml	Wed Aug 03 17:18:47 2022 +0200
     1.3 @@ -271,9 +271,10 @@
     1.4      try_rew ctxt Rewrite_Ord.e_rew_ordX Rule_Set.empty [] f 
     1.5        (Rule.Eval (assoc_calc' (Proof_Context.theory_of ctxt) scrID |> snd))
     1.6    | applicable ctxt ro erls f (Rewrite thm'') =
     1.7 -    try_rew ctxt (ro, Rewrite_Ord.assoc_rew_ord ro) erls [] f (Rule.Thm thm'')
     1.8 +    try_rew ctxt (ro, assoc_rew_ord (Proof_Context.theory_of ctxt) ro) erls [] f (Rule.Thm thm'')
     1.9    | applicable ctxt ro erls f (Rewrite_Inst (subs, thm'')) =
    1.10 -    try_rew ctxt (ro, Rewrite_Ord.assoc_rew_ord ro) erls (Subst.T_from_input ctxt subs) f (Rule.Thm thm'')
    1.11 +    try_rew ctxt (ro, assoc_rew_ord (Proof_Context.theory_of ctxt) ro) erls 
    1.12 +      (Subst.T_from_input ctxt subs) f (Rule.Thm thm'')
    1.13  
    1.14    | applicable thy _ _ f (Rewrite_Set rls') =
    1.15      filter_appl_rews thy [] f (assoc_rls rls')