# HG changeset patch
# User paulson
# Date 1169804889 -3600
# Node ID 3b1da1ff65dfbebe762156de335e33623207089d
# Parent  62753ae847a294ec036920de3baf766fab82103a
Improved debugging

diff -r 62753ae847a2 -r 3b1da1ff65df src/HOL/Tools/ATP/reduce_axiomsN.ML
--- a/src/HOL/Tools/ATP/reduce_axiomsN.ML	Fri Jan 26 10:46:22 2007 +0100
+++ b/src/HOL/Tools/ATP/reduce_axiomsN.ML	Fri Jan 26 10:48:09 2007 +0100
@@ -228,7 +228,8 @@
 	    let val weight = clause_weight ctab rel_consts consts_typs
 	    in
 	      if p <= weight orelse (!follow_defs andalso defines thy clsthm rel_consts)
-	      then (Output.debug (fn () => (name ^ " passes: " ^ Real.toString weight));
+	      then (Output.debug (fn () => (name ^ " clause " ^ Int.toString n ^ 
+	                                    " passes: " ^ Real.toString weight));
 	            relevant ((ax,weight)::newrels, rejects) axs)
 	      else relevant (newrels, ax::rejects) axs
 	    end