tuned msg;
authorwenzelm
Mon, 26 Jun 2000 16:54:38 +0200
changeset 9152 034cb4ac78b8
parent 9151 5339a76c6dfe
child 9153 45f8896faacd
tuned msg;
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]);