changeset 44121 | 44adaa6db327 |
parent 42361 | 23f352990944 |
child 45511 | 9b0f8ca4388e |
--- 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 (*###