do not intercept ML exceptions -- printing exception positions/text is the job of the Isar/ML toplevel;
use up-to-date ML_Compiler.exn_message;

--- a/src/HOL/Import/proof_kernel.ML	Mon Jul 12 18:59:38 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Mon Jul 12 20:21:39 2010 +0200
@@ -175,10 +175,6 @@
 exception PK of string * string
 fun ERR f mesg = PK (f,mesg)
 
-fun print_exn e =
-    case e of
-        PK (m,s) => (writeln ("PK (" ^ m ^ "): " ^ s); raise e)
-      | _ => OldGoals.print_exn e
 
 (* Compatibility. *)
 
@@ -1311,8 +1307,10 @@
                     end
                   | NONE => (thy,NONE)
             end
-    end
-    handle e => (message "Exception in get_isabelle_thm"; if_debug print_exn e handle _ => (); (thy,NONE))
+    end  (* FIXME avoid handle _ *)
+    handle e =>
+      (if_debug (fn () => writeln ("Exception in get_isabelle_thm:\n" ^ ML_Compiler.exn_message e)) ();
+        (thy,NONE))
 
 fun get_isabelle_thm_and_warn thyname thmname hol4conc thy =
   let
@@ -1974,7 +1972,6 @@
     in
         (thy22',hth)
     end
-    handle e => (message "exception in new_definition"; print_exn e)
 
 local
     val helper = thm "termspec_help"
@@ -2056,7 +2053,6 @@
         in
             intern_store_thm false thyname thmname hth thy''
         end
-        handle e => (message "exception in new_specification"; print_exn e)
 
 end
 
@@ -2137,7 +2133,6 @@
         in
             (thy6,hth')
         end
-        handle e => (message "exception in new_type_definition"; print_exn e)
 
 fun add_dump_syntax thy name =
     let
@@ -2230,7 +2225,6 @@
         in
             (thy,hth')
         end
-        handle e => (message "exception in type_introduction"; print_exn e)
 end
 
 val prin = prin

--- a/src/HOL/Import/replay.ML	Mon Jul 12 18:59:38 2010 +0200
+++ b/src/HOL/Import/replay.ML	Mon Jul 12 20:21:39 2010 +0200
@@ -272,12 +272,12 @@
             end
     in
         let
-            val x = rp' prf thy handle e => (writeln "Exception in replay_proof"; OldGoals.print_exn e)
+            val x = rp' prf thy
             val _ = ImportRecorder.stop_replay_proof thyname thmname
         in
             x
         end
-    end handle x => (ImportRecorder.abort_replay_proof thyname thmname; raise x)
+    end handle x => (ImportRecorder.abort_replay_proof thyname thmname; reraise x)
 
 fun setup_int_thms thyname thy =
     let

--- a/src/HOL/Import/shuffler.ML	Mon Jul 12 18:59:38 2010 +0200
+++ b/src/HOL/Import/shuffler.ML	Mon Jul 12 20:21:39 2010 +0200
@@ -219,7 +219,7 @@
         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)))) =
@@ -315,7 +315,7 @@
     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
@@ -340,7 +340,6 @@
                        SOME res
                   end
               else NONE)
-             handle e => OldGoals.print_exn e)
           | _ => NONE
        end
 
@@ -521,7 +520,7 @@
     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. *)
 
@@ -618,7 +617,6 @@
                                         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