1.1 --- a/src/Tools/isac/Interpret/derive.sml	Thu Apr 29 12:43:50 2021 +0200
     1.2 +++ b/src/Tools/isac/Interpret/derive.sml	Thu Apr 29 14:13:11 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 NO_REWRITE => raise ERROR "derive_norm, Eval: no rewrite")
     1.8 +                handle Rewrite.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'