diff -r 4ea3358fac3f -r 5b4247055bd7 src/HOL/Tools/cnf_funcs.ML
--- a/src/HOL/Tools/cnf_funcs.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/Tools/cnf_funcs.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,8 +1,6 @@
 (*  Title:      HOL/Tools/cnf_funcs.ML
-    ID:         $Id$
     Author:     Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
-    Author:     Tjark Weber
-    Copyright   2005-2006
+    Author:     Tjark Weber, TU Muenchen
 
   FIXME: major overlaps with the code in meson.ML
 
@@ -499,7 +497,7 @@
 					NONE
 		in
 			Int.max (max, getOpt (idx, 0))
-		end) (term_frees simp) 0)
+		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
 in