src/HOL/Tools/cnf_funcs.ML

 					val thm1 = make_cnfx_disj_thm x' y1
 					val thm2 = make_cnfx_disj_thm x' y2
 				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 ()
 					val thm2 = make_cnfx_disj_thm (betapply (x', var)) y'  (* (x' | y') = body' *)
 					val thm3 = Thm.forall_intr (cterm_of thy var) thm2     (* !!v. (x' | y') = body' *)
 					val thm4 = Thm.strip_shyps (thm3 COMP allI)            (* ALL v. (x' | y') = body' *)
 					val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *)
 				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 ()
 					val thm2 = make_cnfx_disj_thm x' (betapply (y', var))  (* (x' | y') = body' *)
 					val thm3 = Thm.forall_intr (cterm_of thy var) thm2     (* !!v. (x' | y') = body' *)