# HG changeset patch
# User wenzelm
# Date 1162664741 -3600
# Node ID 4d733b76b5fa8abcd0573487d52a4355e7645247
# Parent  663a7b39894c021ebf8d59e5f0c0297589a4aad4
removed is_Trueprop (use can dest_Trueprop'' instead);

diff -r 663a7b39894c -r 4d733b76b5fa src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Sat Nov 04 19:25:40 2006 +0100
+++ b/src/HOL/Tools/meson.ML	Sat Nov 04 19:25:41 2006 +0100
@@ -250,7 +250,7 @@
   Eliminates existential quantifiers using skoths: Skolemization theorems.*)
 fun cnf skoths (th,ths) =
   let fun cnf_aux (th,ths) =
-  	if not (HOLogic.is_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
+  	if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
         else if not (has_conns ["All","Ex","op &"] (prop_of th))  
 	then th::ths (*no work to do, terminate*)
 	else case head_of (HOLogic.dest_Trueprop (concl_of th)) of