1.1 --- a/src/HOL/Tools/meson.ML Sat May 17 14:27:02 2008 +0200
1.2 +++ b/src/HOL/Tools/meson.ML Sat May 17 15:31:42 2008 +0200
1.3 @@ -625,9 +625,9 @@
1.4 let val horns = make_horns (cls@ths)
1.5 val _ =
1.6 Output.debug (fn () => ("meson method called:\n" ^
1.7 - space_implode "\n" (map Display.string_of_thm (cls@ths)) ^
1.8 + cat_lines (map Display.string_of_thm (cls@ths)) ^
1.9 "\nclauses:\n" ^
1.10 - space_implode "\n" (map Display.string_of_thm horns)))
1.11 + cat_lines (map Display.string_of_thm horns)))
1.12 in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns)
1.13 end
1.14 );