counter added to SAT signature

--- a/src/HOL/Tools/sat_funcs.ML	Wed Oct 12 17:06:22 2005 +0200
+++ b/src/HOL/Tools/sat_funcs.ML	Wed Oct 12 18:17:48 2005 +0200
@@ -55,6 +55,7 @@
 	val trace_sat : bool ref  (* print trace messages *)
 	val sat_tac   : int -> Tactical.tactic
 	val satx_tac  : int -> Tactical.tactic
+	val counter   : int ref  (* number of resolution steps during last proof replay *)
 end
 
 functor SATFunc (structure cnf : CNF) : SAT =