# HG changeset patch
# User wenzelm
# Date 1005845767 -3600
# Node ID 657ad5edeab608da5751fd8d1adb70b34a9ccb53
# Parent  510c3eee55de97884bd636d39bef2a0324ddcba3
prove: raise ERROR_MESSAGE;

diff -r 510c3eee55de -r 657ad5edeab6 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Thu Nov 15 18:35:15 2001 +0100
+++ b/src/Pure/tactic.ML	Thu Nov 15 18:36:07 2001 +0100
@@ -632,8 +632,9 @@
     val fixed_tfrees = foldr Term.add_typ_tfree_names (map #2 fixed_frees, []);
     val params = mapfilter (fn x => apsome (pair x) (assoc_string (frees, x))) xs;
 
-    fun err msg = error (msg ^ "\nThe error(s) above occurred for the goal statement:\n" ^
-      Sign.string_of_term sign (Term.list_all_free (params, statement)));
+    fun err msg = raise ERROR_MESSAGE
+      (msg ^ "\nThe error(s) above occurred for the goal statement:\n" ^
+        Sign.string_of_term sign (Term.list_all_free (params, statement)));
 
     fun cert_safe t = Thm.cterm_of sign (Envir.beta_norm t)
       handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg;