src/HOL/Tools/cnf_funcs.ML

--- a/src/HOL/Tools/cnf_funcs.ML	Tue Oct 20 23:25:04 2009 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML	Wed Oct 21 00:36:12 2009 +0200
@@ -489,7 +489,7 @@
 				else
 					NONE
 		in
-			Int.max (max, getOpt (idx, 0))
+			Int.max (max, the_default 0 idx)
 		end) (OldTerm.term_frees simp) 0)
 	(* finally, convert to definitional CNF (this should preserve the simplification) *)
 	val cnfx_thm = make_cnfx_thm_from_nnf simp