--- a/src/Pure/simplifier.ML Fri Mar 29 22:13:02 2013 +0100
+++ b/src/Pure/simplifier.ML Fri Mar 29 22:14:27 2013 +0100
@@ -121,13 +121,14 @@
let
val pretty_cterm = Syntax.pretty_term ctxt o Thm.term_of;
val pretty_thm = Display.pretty_thm ctxt;
- fun pretty_proc (name, lhss) = Pretty.big_list (name ^ ":") (map pretty_cterm lhss);
+ fun pretty_proc (name, lhss) =
+ Pretty.big_list (name ^ ":") (map (Pretty.item o single o pretty_cterm) lhss);
fun pretty_cong (name, thm) =
Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, pretty_thm thm];
val {simps, procs, congs, loopers, unsafe_solvers, safe_solvers, ...} = dest_ss ss;
in
- [Pretty.big_list "simplification rules:" (map (pretty_thm o #2) simps),
+ [Pretty.big_list "simplification rules:" (map (Pretty.item o single o pretty_thm o #2) simps),
Pretty.big_list "simplification procedures:" (map pretty_proc (sort_wrt #1 procs)),
Pretty.big_list "congruences:" (map pretty_cong congs),
Pretty.strs ("loopers:" :: map quote loopers),