--- 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;