diff -r 47f7bddc3239 -r e9c1574d0caf src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Sat Sep 17 18:11:22 2005 +0200
+++ b/src/HOL/Import/shuffler.ML	Sat Sep 17 18:11:23 2005 +0200
@@ -486,7 +486,6 @@
 be handy in its own right, for example for indexing terms. *)
 
 fun norm_term thy t =
-    PolyML.exception_trace (fn () =>
     let
 	val sg = sign_of thy
 
@@ -509,7 +508,7 @@
 	val _ = message ("norm_term: " ^ (string_of_thm th))
     in
 	th
-    end)
+    end
     handle e => (writeln "norm_term internal error"; print_sign_exn (sign_of thy) e)