# HG changeset patch
# User wenzelm
# Date 998417349 -7200
# Node ID 4c25eef6f3256d95c0d58f61d5698bcd7e005bc3
# Parent  e80a712982e1086fdae0b61d5cd5ffa20f8a020b
tuned error message;

diff -r e80a712982e1 -r 4c25eef6f325 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Thu Aug 16 23:19:12 2001 +0200
+++ b/src/Pure/Isar/args.ML	Tue Aug 21 20:09:09 2001 +0200
@@ -222,7 +222,7 @@
 fun dest_src (Src src) = src;
 
 fun err_in_src kind msg (Src ((s, args), pos)) =
-  error (kind ^ " " ^ s ^ Position.str_of pos ^ ": " ^ msg ^ "\n  " ^
+  error (kind ^ " " ^ quote s ^ Position.str_of pos ^ ": " ^ msg ^ "\n  " ^
     space_implode " " (map str_of args));