tuned;
authorwenzelm
Fri Jan 07 15:55:27 2011 +0100 (2011-01-07)
changeset 414451b31460c2e3a
parent 41444 7f40120cd814
child 41446 92facb553823
tuned;
src/HOL/Tools/Quotient/quotient_info.ML
     1.1 --- a/src/HOL/Tools/Quotient/quotient_info.ML	Fri Jan 07 15:35:00 2011 +0100
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_info.ML	Fri Jan 07 15:55:27 2011 +0100
     1.3 @@ -105,9 +105,9 @@
     1.4  fun print_mapsinfo ctxt =
     1.5    let
     1.6      fun prt_map (ty_name, {mapfun, relmap}) =
     1.7 -      Pretty.block (Library.separate (Pretty.brk 2)
     1.8 +      Pretty.block (separate (Pretty.brk 2)
     1.9          (map Pretty.str
    1.10 -          ["type:", ty_name,
    1.11 +         ["type:", ty_name,
    1.12            "map:", mapfun,
    1.13            "relation map:", relmap]))
    1.14    in
    1.15 @@ -152,7 +152,7 @@
    1.16  fun print_quotinfo ctxt =
    1.17    let
    1.18      fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} =
    1.19 -      Pretty.block (Library.separate (Pretty.brk 2)
    1.20 +      Pretty.block (separate (Pretty.brk 2)
    1.21         [Pretty.str "quotient type:",
    1.22          Syntax.pretty_typ ctxt qtyp,
    1.23          Pretty.str "raw type:",