# HG changeset patch
# User wenzelm
# Date 1006904555 -3600
# Node ID 4e7c3f45a0837a15072bf1855766e92202193fe8
# Parent  459aa05af6bea40b5d4f9febf96d25da684b55d1
print_state: up to 7 result names;

diff -r 459aa05af6be -r 4e7c3f45a083 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Nov 28 00:42:04 2001 +0100
+++ b/src/Pure/Isar/proof.ML	Wed Nov 28 00:42:35 2001 +0100
@@ -348,7 +348,8 @@
 
     fun prt_names names =
       (case filter_out (equal "") names of [] => ""
-      | nms => " " ^ enclose "(" ")" (space_implode " and " nms));
+      | nms => " " ^ enclose "(" ")" (space_implode " and " (take (7, nms) @
+          (if length nms > 7 then ["..."] else []))));
 
     fun prt_goal (_, (i, (((kind, names, _), (goal_facts, thm)), _))) =
       pretty_facts "using " ctxt