# HG changeset patch
# User wenzelm
# Date 1025617227 -7200
# Node ID a02ee4fec6b777fe5352ee3494855f149e638190
# Parent  fdd23370b98fbfcf5380ba666ca3d64af564911f
ProofContext.pretty_fact;

diff -r fdd23370b98f -r a02ee4fec6b7 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Tue Jul 02 15:39:49 2002 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Tue Jul 02 15:40:27 2002 +0200
@@ -309,12 +309,9 @@
 
 local
 
-fun prt_fact ctxt ("", ths) = ProofContext.pretty_thms ctxt ths
-  | prt_fact ctxt (name, ths) =
-      Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, ProofContext.pretty_thms ctxt ths];
-
 fun prt_facts ctxt =
-  flat o (separate [Pretty.fbrk, Pretty.str "and "]) o map (single o prt_fact ctxt);
+  flat o (separate [Pretty.fbrk, Pretty.str "and "]) o
+    map (single o ProofContext.pretty_fact ctxt);
 
 fun pretty_results ctxt ((kind, ""), facts) =
       Pretty.block (Pretty.str kind :: Pretty.brk 1 :: prt_facts ctxt facts)