1.1 --- a/src/Tools/isac/Interpret/derive.sml	Tue Apr 27 18:14:02 2021 +0200
     1.2 +++ b/src/Tools/isac/Interpret/derive.sml	Tue Apr 27 19:52:29 2021 +0200
     1.3 @@ -94,7 +94,7 @@
     1.4                  val _ = msg_5 t'
     1.5                  val r' = Rule.Thm (thmid, tm)
     1.6                in rew_once (lim - 1) (rts @ [(t, r', (t', a'))]) t' Appl rrs' end) 
     1.7 -                handle _ => raise ERROR "derive_norm, Eval: no rewrite")
     1.8 +                handle NO_REWRITE => raise ERROR "derive_norm, Eval: no rewrite")
     1.9          | Rule.Rls_ rls =>
    1.10            (case Rewrite.rewrite_set_ thy true rls t of
    1.11              NONE => rew_once lim rts t apno rs'