src/HOL/Import/shuffler.ML

         val lhs = list_all ([xv,yv],t)
         val rhs = list_all ([yv,xv],swap_bound 0 t)
         val rew = Logic.mk_equals (lhs,rhs)
         val init = Thm.trivial (cterm_of thy rew)
     in
-        (all_comm RS init handle e => (message "rew_th"; OldGoals.print_exn e))
+        all_comm RS init
     end
 
 fun quant_rewrite thy assumes (t as Const("all",T1) $ (Abs(x,xT,Const("all",T2) $ Abs(y,yT,body)))) =
     let
         val res = (find_bound 0 body;2) handle RESULT i => i

                 else ()
             end
     in
         case t of
             Const("all",_) $ (Abs(x,xT,Const("==",eqT) $ P $ Q)) =>
-            ((if eta_redex P andalso eta_redex Q
+            (if eta_redex P andalso eta_redex Q
               then
                   let
                       val cert = cterm_of thy
                       val v = Free (Name.variant (Term.add_free_names t []) "v", xT)
                       val cv = cert v

                       val lhs = (#1 (Logic.dest_equals (prop_of res)))
                   in
                        SOME res
                   end
               else NONE)
-             handle e => OldGoals.print_exn e)
           | _ => NONE
        end
 
 fun beta_fun thy assume t =
     SOME (Thm.beta_conversion true (cterm_of thy t))

         val c = prop_of th
         val vars = OldTerm.add_term_frees (c, OldTerm.add_term_vars(c,[]))
     in
         Drule.forall_intr_list (map (cterm_of thy) vars) th
     end
-    handle e => (writeln "close_thm internal error"; OldGoals.print_exn e)
+
 
 (* Normalizes a theorem's conclusion using norm_term. *)
 
 fun norm_thm thy th =
     let

                res as SOME (name,th) => if (prop_of th) aconv t
                                         then res
                                         else error "Internal error in set_prop"
              | NONE => NONE
     end
-    handle e => (writeln "set_prop internal error"; OldGoals.print_exn e)
 
 fun find_potential thy t =
     let
         val shuffles = ShuffleData.get thy
         val ignored = collect_ignored shuffles []