Now prove_goalw_cterm calls print_sign_exn_unit, so that the rest
of the error message ("The exception above was raised for...") will appear.
And print_exn calls print_sign_exn_unit so that it can re-raise the SAME
exception.

--- a/src/Pure/goals.ML	Mon Feb 27 18:05:38 1995 +0100
+++ b/src/Pure/goals.ML	Mon Feb 27 18:07:59 1995 +0100
@@ -201,7 +201,7 @@
 	       Some(st,_) => st
 	     | _ => error ("prove_goal: tactic failed"))
   in  mkresult (true, cond_timeit (!proof_timing) statef)  end
-  handle e => (print_sign_exn (#sign (rep_cterm chorn)) e;
+  handle e => (print_sign_exn_unit (#sign (rep_cterm chorn)) e;
 	       error ("The exception above was raised for\n" ^ 
 		      string_of_cterm chorn));
 
@@ -439,7 +439,7 @@
 
 (*Prints exceptions nicely at top level; 
   raises the exception in order to have a polymorphic type!*)
-fun print_exn e = (print_sign_exn (top_sg()) e;  raise e);
+fun print_exn e = (print_sign_exn_unit (top_sg()) e;  raise e);
 
 end;
 end;