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