changeset 55239 | 97921d23ebe3 |
parent 55236 | 8d61b0aa7a0d |
child 55523 | 9429e7b5b827 |
--- a/src/HOL/Tools/Meson/meson_clausify.ML Sat Feb 01 20:46:19 2014 +0100 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Sat Feb 01 21:09:53 2014 +0100 @@ -222,7 +222,7 @@ fun to_definitional_cnf_with_quantifiers ctxt th = let - val eqth = cnf.make_cnfx_thm ctxt (HOLogic.dest_Trueprop (prop_of th)) + val eqth = CNF.make_cnfx_thm ctxt (HOLogic.dest_Trueprop (prop_of th)) val eqth = eqth RS @{thm eq_reflection} val eqth = eqth RS @{thm TruepropI} in Thm.equal_elim eqth th end