tuned error msg;
authorwenzelm
Thu, 28 May 1998 11:09:07 +0200
changeset 4975 20b89fcd90a7
parent 4974 45b7a51342a1
child 4976 19f48dafe5d3
tuned error msg;
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);