diff -r 5c3e9415c653 -r fce7b764cbd6 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Wed Oct 19 21:52:32 2005 +0200
+++ b/src/HOL/Tools/record_package.ML	Wed Oct 19 21:52:33 2005 +0200
@@ -1479,8 +1479,7 @@
                             [(cterm_of sg v,cterm_of sg v'),
                              (cterm_of sg r,cterm_of sg ext)] udef;
           in  standard (Thm.transitive udef' bdyeq) end;
-      in map mkthm (rev upd_defs  ~~ (mixit dest_convs' refls))
-         handle e => print_exn e end;
+      in map mkthm (rev upd_defs  ~~ (mixit dest_convs' refls)) end;
 
     val upd_convs_prf = quick_and_dirty_prf upd_convs_prf_noopt upd_convs_prf_opt;