# HG changeset patch
# User wenzelm
# Date 1294412127 -3600
# Node ID 1b31460c2e3a36e63ca259a3bc2ad18c06226912
# Parent  7f40120cd814618ae40bfec33af0b2e11444ded4
tuned;

diff -r 7f40120cd814 -r 1b31460c2e3a src/HOL/Tools/Quotient/quotient_info.ML
--- a/src/HOL/Tools/Quotient/quotient_info.ML	Fri Jan 07 15:35:00 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_info.ML	Fri Jan 07 15:55:27 2011 +0100
@@ -105,9 +105,9 @@
 fun print_mapsinfo ctxt =
   let
     fun prt_map (ty_name, {mapfun, relmap}) =
-      Pretty.block (Library.separate (Pretty.brk 2)
+      Pretty.block (separate (Pretty.brk 2)
         (map Pretty.str
-          ["type:", ty_name,
+         ["type:", ty_name,
           "map:", mapfun,
           "relation map:", relmap]))
   in
@@ -152,7 +152,7 @@
 fun print_quotinfo ctxt =
   let
     fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} =
-      Pretty.block (Library.separate (Pretty.brk 2)
+      Pretty.block (separate (Pretty.brk 2)
        [Pretty.str "quotient type:",
         Syntax.pretty_typ ctxt qtyp,
         Pretty.str "raw type:",