src/HOL/Tools/res_hol_clause.ML
changeset 32955 4a78daeb012b
parent 32529 d703a76acc08
child 32960 69916a850301
     1.1 --- a/src/HOL/Tools/res_hol_clause.ML	Fri Oct 16 00:26:19 2009 +0200
     1.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Fri Oct 16 10:45:10 2009 +0200
     1.3 @@ -459,7 +459,7 @@
     1.4    fold count_constants_lit literals (const_min_arity, const_needs_hBOOL);
     1.5  
     1.6  fun display_arity const_needs_hBOOL (c,n) =
     1.7 -  Output.debug (fn () => "Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^
     1.8 +  ResAxioms.trace_msg (fn () => "Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^
     1.9                  (if needs_hBOOL const_needs_hBOOL c then " needs hBOOL" else ""));
    1.10  
    1.11  fun count_constants (conjectures, _, extra_clauses, helper_clauses, _, _) =