# HG changeset patch
# User blanchet
# Date 1283418133 -7200
# Node ID 094848cf7ef3b8485a641e3f70fa81b7a25fa8f0
# Parent  e820beaf7d8cc60de099ea5179778f6247940528
make definitional CNF translation code more robust in the presence of existential quantifiers in the "literals"

diff -r e820beaf7d8c -r 094848cf7ef3 src/HOL/Tools/cnf_funcs.ML
--- a/src/HOL/Tools/cnf_funcs.ML	Thu Sep 02 08:51:16 2010 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML	Thu Sep 02 11:02:13 2010 +0200
@@ -430,7 +430,7 @@
 				in
 					make_cnf_disj_conj_r OF [thm1, thm2]  (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *)
 				end
-			  | make_cnfx_disj_thm (Const (@{const_name Ex}, _) $ x') y' =
+			  | make_cnfx_disj_thm (@{term "Ex::(bool => bool) => bool"} $ x') y' =
 				let
 					val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_l   (* ((Ex x') | y') = (Ex (x' | y')) *)
 					val var  = new_free ()
@@ -441,7 +441,7 @@
 				in
 					iff_trans OF [thm1, thm5]  (* ((Ex x') | y') = (Ex v. body') *)
 				end
-			  | make_cnfx_disj_thm x' (Const (@{const_name Ex}, _) $ y') =
+			  | make_cnfx_disj_thm x' (@{term "Ex::(bool => bool) => bool"} $ y') =
 				let
 					val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_r   (* (x' | (Ex y')) = (Ex (x' | y')) *)
 					val var  = new_free ()