# HG changeset patch
# User wenzelm
# Date 1394486900 -3600
# Node ID 98d466e6de8ae916b2b522af7efc392a86ae0214
# Parent  5ff5208de089e1ed3df6a70c048c246288904dd4
tuned message;

diff -r 5ff5208de089 -r 98d466e6de8a src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Mar 10 22:22:03 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Mon Mar 10 22:28:20 2014 +0100
@@ -441,7 +441,7 @@
 
 fun check_type_name {proper, strict} ctxt (c, pos) =
   if Lexicon.is_tid c then
-    if proper then error ("Not a type constructor: " ^ c ^ Position.here pos)
+    if proper then error ("Not a type constructor: " ^ quote c ^ Position.here pos)
     else
       let
         val reports =