src/HOL/Tools/inductive_codegen.ML

   (fn NONE => "X"
     | SOME js => enclose "[" "]" (commas (map string_of_int js)))
        (iss @ [SOME is]));
 
 fun print_modes modes = message ("Inferred modes:\n" ^
-  space_implode "\n" (map (fn (s, ms) => s ^ ": " ^ commas (map
+  cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
     string_of_mode ms)) modes));
 
 val term_vs = map (fst o fst o dest_Var) o term_vars;
 val terms_vs = distinct (op =) o List.concat o (map term_vs);
 

 fun lookup_modes gr dep = apfst List.concat (apsnd List.concat (ListPair.unzip
   (map ((fn (SOME (Modes x), _, _) => x | _ => ([], [])) o get_node gr)
     (Graph.all_preds (fst gr) [dep]))));
 
 fun print_arities arities = message ("Arities:\n" ^
-  space_implode "\n" (map (fn (s, (ks, k)) => s ^ ": " ^
+  cat_lines (map (fn (s, (ks, k)) => s ^ ": " ^
     space_implode " -> " (map
       (fn NONE => "X" | SOME k' => string_of_int k')
         (ks @ [SOME k]))) arities));
 
 fun prep_intrs intrs = map (rename_term o #prop o rep_thm o standard) intrs;