author | wenzelm |
Sat, 17 Sep 2005 18:11:23 +0200 | |
changeset 17463 | e9c1574d0caf |
parent 17462 | 47f7bddc3239 |
child 17464 | a4090ccf14a8 |
--- 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)