# HG changeset patch
# User lcp
# Date 777225208 -7200
# Node ID fc4ff96bb0e93b6e467224ada57c4b023c0ddca0
# Parent  c53386a5bcf18d2903f6e00feec8c1c05111bb6a
Pure/goals.ML: prove_goalw_cterm now does its own exception-handling, moved
from prove_goalw

diff -r c53386a5bcf1 -r fc4ff96bb0e9 src/Pure/goals.ML
--- a/src/Pure/goals.ML	Thu Aug 18 17:50:22 1994 +0200
+++ b/src/Pure/goals.ML	Thu Aug 18 17:53:28 1994 +0200
@@ -194,18 +194,19 @@
 	  (case Sequence.pull (tapply(tac,st0)) of 
 	       Some(st,_) => st
 	     | _ => error ("prove_goal: tactic failed"))
-  in  mkresult (true, cond_timeit (!proof_timing) statef)  end;
+  in  mkresult (true, cond_timeit (!proof_timing) statef)  end
+  handle e => (print_sign_exn (#sign (rep_cterm chorn)) e;
+	       error ("The exception above was raised for\n" ^ 
+		      string_of_cterm chorn));
+
 
 (*Version taking the goal as a string*)
 fun prove_goalw thy rths agoal tacsf =
   let val sign = sign_of thy
       val chorn = read_cterm sign (agoal,propT)
-  in  prove_goalw_cterm rths chorn tacsf  
-      handle ERROR => error (*from type_assign, etc via prepare_proof*)
-		("The error above occurred for " ^ quote agoal)
-       | e => (print_sign_exn sign e;	(*other exceptions*)
-	       error ("The exception above was raised for " ^ quote agoal))
-  end;
+  in  prove_goalw_cterm rths chorn tacsf end
+  handle ERROR => error (*from read_cterm?*)
+		("The error above occurred for " ^ quote agoal);
 
 (*String version with no meta-rewrite-rules*)
 fun prove_goal thy = prove_goalw thy [];