# HG changeset patch
# User wenzelm
# Date 869227614 -7200
# Node ID 8fb4150e2ad35e31f557334dd0ac707fd3a0bf9d
# Parent  19bd6c8274c40d2a46e1bfd7cdad07be72ee75f0
tuned error propagation msg;

diff -r 19bd6c8274c4 -r 8fb4150e2ad3 src/Pure/goals.ML
--- a/src/Pure/goals.ML	Fri Jul 18 13:57:19 1997 +0200
+++ b/src/Pure/goals.ML	Fri Jul 18 14:06:54 1997 +0200
@@ -215,7 +215,7 @@
       val chorn = read_cterm sign (agoal,propT)
   in  prove_goalw_cterm rths chorn tacsf end
   handle ERROR => error (*from read_cterm?*)
-		("The error above occurred for " ^ quote agoal);
+		("The error(s) above occurred for " ^ quote agoal);
 
 (*String version with no meta-rewrite-rules*)
 fun prove_goal thy = prove_goalw thy [];
@@ -318,7 +318,7 @@
 fun goalw thy rths agoal = 
   goalw_cterm rths (read_cterm(sign_of thy)(agoal,propT))
   handle ERROR => error (*from type_assign, etc via prepare_proof*)
-	    ("The error above occurred for " ^ quote agoal);
+	    ("The error(s) above occurred for " ^ quote agoal);
 
 (*String version with no meta-rewrite-rules*)
 fun goal thy = goalw thy [];
diff -r 19bd6c8274c4 -r 8fb4150e2ad3 src/Pure/section_utils.ML
--- a/src/Pure/section_utils.ML	Fri Jul 18 13:57:19 1997 +0200
+++ b/src/Pure/section_utils.ML	Fri Jul 18 14:06:54 1997 +0200
@@ -27,7 +27,7 @@
 (*Read a term from string "b", with expected type T*)
 fun readtm sign T b = 
     read_cterm sign (b,T) |> term_of
-    handle ERROR => error ("The error above occurred for " ^ b);
+    handle ERROR => error ("The error(s) above occurred for " ^ b);
 
 (*From HOL/ex/meson.ML: raises exception if no rules apply -- unlike RL*)
 fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))