src/HOL/Tools/meson.ML
changeset 26931 aa226d8405a8
parent 26928 ca87aff1ad2d
child 27153 56b6cdce22f1
     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   );