src/HOLCF/Tools/Domain/domain_theorems.ML

       in (finites, ind) end
   )
       handle THM _ =>
              (warning "Induction proofs failed (THM raised)."; ([], TrueI))
            | ERROR _ =>
-             (warning "Induction proofs failed (ERROR raised)."; ([], TrueI));
+             (warning "Cannot prove induction rule"; ([], TrueI));
 
 
 end; (* local *)
 
 (* ----- theorem concerning coinduction ------------------------------------- *)