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