diff -r 15865e0c5598 -r 9ce5de06cd3b src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Tue Sep 22 22:38:22 2015 +0200
+++ b/src/Pure/Isar/proof_display.ML	Tue Sep 22 22:42:48 2015 +0200
@@ -85,7 +85,7 @@
 
     val const_space = Proof_Context.const_space ctxt;
     val type_space = Proof_Context.type_space ctxt;
-    val item_space = fn Defs.Constant => const_space | Defs.Type => type_space;
+    val item_space = fn Defs.Const => const_space | Defs.Type => type_space;
     fun prune_item (k, c) = not verbose andalso Name_Space.is_concealed (item_space k) c;
 
     fun markup_extern_item (kind, name) =