removed print_exn (better let the toplevel do this);
authorwenzelm
Wed, 19 Oct 2005 21:52:33 +0200
changeset 17921 fce7b764cbd6
parent 17920 5c3e9415c653
child 17922 0cba8edb269e
removed print_exn (better let the toplevel do this);
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;