src/HOL/Tools/cnf_funcs.ML
changeset 33035 15eab423e573
parent 32960 69916a850301
child 36614 b6c031ad3690
     1.1 --- a/src/HOL/Tools/cnf_funcs.ML	Tue Oct 20 23:25:04 2009 +0200
     1.2 +++ b/src/HOL/Tools/cnf_funcs.ML	Wed Oct 21 00:36:12 2009 +0200
     1.3 @@ -489,7 +489,7 @@
     1.4  				else
     1.5  					NONE
     1.6  		in
     1.7 -			Int.max (max, getOpt (idx, 0))
     1.8 +			Int.max (max, the_default 0 idx)
     1.9  		end) (OldTerm.term_frees simp) 0)
    1.10  	(* finally, convert to definitional CNF (this should preserve the simplification) *)
    1.11  	val cnfx_thm = make_cnfx_thm_from_nnf simp