diff -r 01de796250a0 -r 44adaa6db327 src/HOL/Tools/cnf_funcs.ML
--- a/src/HOL/Tools/cnf_funcs.ML	Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML	Wed Aug 10 20:53:43 2011 +0200
@@ -511,7 +511,7 @@
             NONE
       in
         Int.max (max, the_default 0 idx)
-      end) (OldTerm.term_frees simp) 0)
+      end) (Misc_Legacy.term_frees simp) 0)
     (* finally, convert to definitional CNF (this should preserve the simplification) *)
     val cnfx_thm = make_under_quantifiers ctxt make_cnfx_thm_from_nnf simp
 (*###