src/Pure/Isar/proof_display.ML
changeset 33643 b275f26a638b
parent 33515 d066e8369a33
child 36610 bafd82950e24
--- a/src/Pure/Isar/proof_display.ML	Thu Nov 12 21:59:35 2009 +0100
+++ b/src/Pure/Isar/proof_display.ML	Thu Nov 12 22:02:11 2009 +0100
@@ -91,7 +91,7 @@
 in
 
 fun print_results do_print ctxt ((kind, name), facts) =
-  if not do_print orelse kind = "" orelse kind = Thm.internalK then ()
+  if not do_print orelse kind = "" then ()
   else if name = "" then
     Pretty.writeln (Pretty.block (Pretty.str kind :: Pretty.brk 1 :: pretty_facts ctxt facts))
   else Pretty.writeln