src/HOL/Tools/Quotient/quotient_info.ML

     "declaration of map information"))
 
 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
     MapsData.get (ProofContext.theory_of ctxt)
     |> Symtab.dest

   map snd (Symtab.dest (QuotData.get (ProofContext.theory_of lthy)))
 
 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:",
         Syntax.pretty_typ ctxt rtyp,
         Pretty.str "relation:",