# HG changeset patch
# User wenzelm
# Date 931635308 -7200
# Node ID 54d4d16020689d070d25705c5e124b9b9b0ade97
# Parent  d33b1629eaf9b052c57a4c00ad96002a216f80cb
prove_goalw_cterm_general: pass exeption;

diff -r d33b1629eaf9 -r 54d4d1602068 src/Pure/goals.ML
--- a/src/Pure/goals.ML	Sat Jul 10 21:34:01 1999 +0200
+++ b/src/Pure/goals.ML	Sat Jul 10 21:35:08 1999 +0200
@@ -275,8 +275,8 @@
 	     | _ => error ("prove_goal: tactic failed"))
   in  mkresult (check, cond_timeit (!proof_timing) statef)  end
   handle e => (print_sign_exn_unit (#sign (rep_cterm chorn)) e;
-	       error ("The exception above was raised for\n" ^ 
-		      string_of_cterm chorn));
+	       writeln ("The exception above was raised for\n" ^ 
+		      string_of_cterm chorn); raise e);
 
 (*Two variants: one checking the result, one not.  
   Neither prints runtime messages: they are for internal packages.*)