src/HOL/Import/shuffler.ML

 (* Transforms a term t to some normal form t', returning the theorem t
 == t'.  This is originally a help function for make_equal, but might
 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
 
 	val norms = ShuffleData.get thy
 	val ss = empty_ss setmksimps single

 	      |> chain eta_conversion
 	      |> strip_shyps
 	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)
 
 
 (* Closes a theorem with respect to free and schematic variables (does
 not touch type variables, though). *)