--- 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)