# HG changeset patch
# User wenzelm
# Date 962031278 -7200
# Node ID 034cb4ac78b83ef9d6001e31be9688a8f9ed8378
# Parent  5339a76c6dfe230cd903e521fe89404c13310b6f
tuned msg;

diff -r 5339a76c6dfe -r 034cb4ac78b8 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon Jun 26 16:54:21 2000 +0200
+++ b/src/Pure/Isar/toplevel.ML	Mon Jun 26 16:54:38 2000 +0200
@@ -378,7 +378,7 @@
   | exn_message (Library.LIST msg) = raised_msg "Library.LIST" msg
   | exn_message exn = General.exnMessage exn
 and fail_message kind ((name, pos), exn) =
-  "Error in " ^ kind ^ " " ^ name ^ Position.str_of pos ^ ":\n" ^ exn_message exn;
+  "Error in " ^ kind ^ " " ^ quote name ^ Position.str_of pos ^ ":\n" ^ exn_message exn;
 
 fun print_exn None = ()
   | print_exn (Some (exn, s)) = error_msg (cat_lines [exn_message exn, s]);