src/HOL/Import/shuffler.ML
changeset 17463 e9c1574d0caf
parent 17440 df77edc4f5d0
child 17892 62c397c17d18
     1.1 --- a/src/HOL/Import/shuffler.ML	Sat Sep 17 18:11:22 2005 +0200
     1.2 +++ b/src/HOL/Import/shuffler.ML	Sat Sep 17 18:11:23 2005 +0200
     1.3 @@ -486,7 +486,6 @@
     1.4  be handy in its own right, for example for indexing terms. *)
     1.5  
     1.6  fun norm_term thy t =
     1.7 -    PolyML.exception_trace (fn () =>
     1.8      let
     1.9  	val sg = sign_of thy
    1.10  
    1.11 @@ -509,7 +508,7 @@
    1.12  	val _ = message ("norm_term: " ^ (string_of_thm th))
    1.13      in
    1.14  	th
    1.15 -    end)
    1.16 +    end
    1.17      handle e => (writeln "norm_term internal error"; print_sign_exn (sign_of thy) e)
    1.18  
    1.19