src/Pure/simplifier.ML
changeset 51580 64ef8260dc60
parent 50107 289181e3e524
child 51584 98029ceda8ce
     1.1 --- a/src/Pure/simplifier.ML	Fri Mar 29 22:13:02 2013 +0100
     1.2 +++ b/src/Pure/simplifier.ML	Fri Mar 29 22:14:27 2013 +0100
     1.3 @@ -121,13 +121,14 @@
     1.4    let
     1.5      val pretty_cterm = Syntax.pretty_term ctxt o Thm.term_of;
     1.6      val pretty_thm = Display.pretty_thm ctxt;
     1.7 -    fun pretty_proc (name, lhss) = Pretty.big_list (name ^ ":") (map pretty_cterm lhss);
     1.8 +    fun pretty_proc (name, lhss) =
     1.9 +      Pretty.big_list (name ^ ":") (map (Pretty.item o single o pretty_cterm) lhss);
    1.10      fun pretty_cong (name, thm) =
    1.11        Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, pretty_thm thm];
    1.12  
    1.13      val {simps, procs, congs, loopers, unsafe_solvers, safe_solvers, ...} = dest_ss ss;
    1.14    in
    1.15 -    [Pretty.big_list "simplification rules:" (map (pretty_thm o #2) simps),
    1.16 +    [Pretty.big_list "simplification rules:" (map (Pretty.item o single o pretty_thm o #2) simps),
    1.17        Pretty.big_list "simplification procedures:" (map pretty_proc (sort_wrt #1 procs)),
    1.18        Pretty.big_list "congruences:" (map pretty_cong congs),
    1.19        Pretty.strs ("loopers:" :: map quote loopers),