# HG changeset patch
# User wenzelm
# Date 750079801 -3600
# Node ID deb04a336a99f3857520526fb752a80727034301
# Parent  4433428596f966e02322ec1ef5be800e852bc9e6
"The error/exception above ...": errorneous goal now quoted;

diff -r 4433428596f9 -r deb04a336a99 src/Pure/goals.ML
--- a/src/Pure/goals.ML	Thu Oct 07 11:47:50 1993 +0100
+++ b/src/Pure/goals.ML	Fri Oct 08 12:30:01 1993 +0100
@@ -1,4 +1,4 @@
-(*  Title: 	goals
+(*  Title: 	Pure/goals.ML
     ID:         $Id$
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
@@ -202,9 +202,9 @@
       val chorn = Sign.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 " ^ agoal)
+		("The error above occurred for " ^ quote agoal)
        | e => (print_sign_exn sign e;	(*other exceptions*)
-	       error ("The exception above was raised for " ^ agoal))
+	       error ("The exception above was raised for " ^ quote agoal))
   end;
 
 (*String version with no meta-rewrite-rules*)
@@ -300,7 +300,7 @@
 fun goalw thy rths agoal = 
   goalw_cterm rths (Sign.read_cterm(sign_of thy)(agoal,propT))
   handle ERROR => error (*from type_assign, etc via prepare_proof*)
-	    ("The error above occurred for " ^ agoal);
+	    ("The error above occurred for " ^ quote agoal);
 
 (*String version with no meta-rewrite-rules*)
 fun goal thy = goalw thy [];