# HG changeset patch
# User wenzelm
# Date 1294841366 -3600
# Node ID c704c437ec741fd923920fc0a82dc905a73751a9
# Parent  3470b54e95d6c3c28cd06c17ff05b03a816dcb51
eliminated obsolete print_sign_exn_unit;

diff -r 3470b54e95d6 -r c704c437ec74 src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Wed Jan 12 15:08:21 2011 +0100
+++ b/src/HOL/Import/shuffler.ML	Wed Jan 12 15:09:26 2011 +0100
@@ -35,27 +35,6 @@
 fun if_debug f x = if !debug then f x else ()
 val message = if_debug writeln
 
-(*Prints exceptions readably to users*)
-fun print_sign_exn_unit sign e =
-  case e of
-     THM (msg,i,thms) =>
-         (writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg);
-          List.app (writeln o Display.string_of_thm_global sign) thms)
-   | THEORY (msg,thys) =>
-         (writeln ("Exception THEORY raised:\n" ^ msg);
-          List.app (writeln o Context.str_of_thy) thys)
-   | TERM (msg,ts) =>
-         (writeln ("Exception TERM raised:\n" ^ msg);
-          List.app (writeln o Syntax.string_of_term_global sign) ts)
-   | TYPE (msg,Ts,ts) =>
-         (writeln ("Exception TYPE raised:\n" ^ msg);
-          List.app (writeln o Syntax.string_of_typ_global sign) Ts;
-          List.app (writeln o Syntax.string_of_term_global sign) ts)
-   | e => raise e
-
-(*Prints an exception, then fails*)
-fun print_sign_exn sign e = (print_sign_exn_unit sign e; raise e)
-
 val string_of_thm = Print_Mode.setmp [] Display.string_of_thm_without_context;
 
 fun mk_meta_eq th =
@@ -506,7 +485,6 @@
     in
         th
     end
-    handle e => (writeln "norm_term internal error"; print_sign_exn thy e)
 
 
 (* Closes a theorem with respect to free and schematic variables (does