1.1 --- a/src/HOL/Tools/inductive_codegen.ML	Sat May 17 14:27:02 2008 +0200
     1.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Sat May 17 15:31:42 2008 +0200
     1.3 @@ -126,7 +126,7 @@
     1.4         (iss @ [SOME is]));
     1.5  
     1.6  fun print_modes modes = message ("Inferred modes:\n" ^
     1.7 -  space_implode "\n" (map (fn (s, ms) => s ^ ": " ^ commas (map
     1.8 +  cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
     1.9      string_of_mode ms)) modes));
    1.10  
    1.11  val term_vs = map (fst o fst o dest_Var) o term_vars;
    1.12 @@ -471,7 +471,7 @@
    1.13      (Graph.all_preds (fst gr) [dep]))));
    1.14  
    1.15  fun print_arities arities = message ("Arities:\n" ^
    1.16 -  space_implode "\n" (map (fn (s, (ks, k)) => s ^ ": " ^
    1.17 +  cat_lines (map (fn (s, (ks, k)) => s ^ ": " ^
    1.18      space_implode " -> " (map
    1.19        (fn NONE => "X" | SOME k' => string_of_int k')
    1.20          (ks @ [SOME k]))) arities));