1.1 --- a/src/Tools/isac/Interpret/derive.sml	Fri Aug 05 11:41:06 2022 +0200
     1.2 +++ b/src/Tools/isac/Interpret/derive.sml	Fri Aug 05 12:30:16 2022 +0200
     1.3 @@ -84,7 +84,7 @@
     1.4                (msg_3 ctxt t'; rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs'))
     1.5          | Rule.Eval (c as (op_, _)) => 
     1.6              (msg_4 ctxt op_;
     1.7 -            case Eval.adhoc_thm (Proof_Context.theory_of ctxt) c t of
     1.8 +            case Eval.adhoc_thm ctxt c t of
     1.9                NONE => rew_once lim rts t apno rs'
    1.10              | SOME (thmid, tm) => 
    1.11                (let