1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml	Fri Aug 05 11:41:06 2022 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml	Fri Aug 05 12:30:16 2022 +0200
     1.3 @@ -249,11 +249,11 @@
     1.4  	    SOME _ => [rule2tac ctxt [] thm']
     1.5  	  | NONE => [])
     1.6    | try_rew ctxt _ _ _ f (cal as Rule.Eval c) = 
     1.7 -    (case Eval.adhoc_thm (Proof_Context.theory_of ctxt) c f of
     1.8 +    (case Eval.adhoc_thm ctxt c f of
     1.9  	    SOME _ => [rule2tac ctxt [] cal]
    1.10      | NONE => [])
    1.11    | try_rew ctxt _ _ _ f (cal as Rule.Cal1 c) = 
    1.12 -    (case Eval.adhoc_thm (Proof_Context.theory_of ctxt) c f of
    1.13 +    (case Eval.adhoc_thm ctxt c f of
    1.14  	      SOME _ => [rule2tac ctxt [] cal]
    1.15        | NONE => [])
    1.16    | try_rew thy _ _ subst f (Rule.Rls_ rls) = filter_appl_rews thy subst f rls