1.1 --- a/src/Tools/isac/Interpret/derive.sml	Mon Jul 19 17:29:35 2021 +0200
     1.2 +++ b/src/Tools/isac/Interpret/derive.sml	Mon Jul 19 18:29:46 2021 +0200
     1.3 @@ -84,7 +84,7 @@
     1.4                (msg_3 t'; rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs'))
     1.5          | Rule.Eval (c as (op_, _)) => 
     1.6              (msg_4 op_;
     1.7 -            case Eval.adhoc_thm thy c (TermC.uminus_to_string t) of
     1.8 +            case Eval.adhoc_thm thy c t of
     1.9                NONE => rew_once lim rts t apno rs'
    1.10              | SOME (thmid, tm) => 
    1.11                (let