changeset 17463 | e9c1574d0caf |
parent 17440 | df77edc4f5d0 |
child 17892 | 62c397c17d18 |
--- 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)