1.1 --- a/src/HOL/Tools/meson.ML	Sat Jan 20 14:09:12 2007 +0100
     1.2 +++ b/src/HOL/Tools/meson.ML	Sat Jan 20 14:09:14 2007 +0100
     1.3 @@ -271,7 +271,7 @@
     1.4        and cnf_nil th = cnf_aux (th,[])
     1.5    in 
     1.6      if too_many_clauses (concl_of th) 
     1.7 -    then (Output.debug ("cnf is ignoring: " ^ string_of_thm th); ths)
     1.8 +    then (Output.debug (fn () => ("cnf is ignoring: " ^ string_of_thm th)); ths)
     1.9      else cnf_aux (th,ths)
    1.10    end;
    1.11  
    1.12 @@ -574,12 +574,11 @@
    1.13  	   [] => no_tac  (*no goal clauses*)
    1.14  	 | goes => 
    1.15  	     let val horns = make_horns (cls@ths)
    1.16 -	         val _ = if !Output.show_debug_msgs 
    1.17 -	                 then Output.debug ("meson method called:\n" ^ 
    1.18 +	         val _ =
    1.19 +	             Output.debug (fn () => ("meson method called:\n" ^ 
    1.20  	     	                  space_implode "\n" (map string_of_thm (cls@ths)) ^ 
    1.21  	     	                  "\nclauses:\n" ^ 
    1.22 -	     	                  space_implode "\n" (map string_of_thm horns))
    1.23 -	     	         else ()
    1.24 +	     	                  space_implode "\n" (map string_of_thm horns)))
    1.25  	     in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns)
    1.26  	     end
    1.27   );