# HG changeset patch
# User wenzelm
# Date 896346547 -7200
# Node ID 20b89fcd90a7721a085b78bed6478c0dd01a5a4c
# Parent  45b7a51342a1a74c862f426bc8abdab33307018e
tuned error msg;

diff -r 45b7a51342a1 -r 20b89fcd90a7 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Thu May 28 11:08:45 1998 +0200
+++ b/src/Pure/Thy/thy_info.ML	Thu May 28 11:09:07 1998 +0200
@@ -63,7 +63,7 @@
 (* retrieve info *)
 
 fun err_not_stored name =
-  error ("Theory " ^ name ^ " not stored by loader");
+  error ("Theory " ^ quote name ^ " not stored by loader");
 
 fun get_thyinfo name = Symtab.lookup (! loaded_thys, name);