1.1 --- a/src/HOL/Tools/meson.ML	Sun Oct 01 22:19:24 2006 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Mon Oct 02 17:29:42 2006 +0200
     1.3 @@ -203,6 +203,8 @@
     1.4    presumably to instantiate a Boolean variable.*)
     1.5  fun resop nf [prem] = resolve_tac (nf prem) 1;
     1.6  
     1.7 +(*Any need to extend this list with 
     1.8 +  "HOL.type_class","OperationalEquality.eq_class","ProtoPure.term"?*)
     1.9  val has_meta_conn = 
    1.10      exists_Const (fn (c,_) => c mem_string ["==", "==>", "all", "prop"]);
    1.11  
    1.12 @@ -216,7 +218,7 @@
    1.13    Eliminates existential quantifiers using skoths: Skolemization theorems.*)
    1.14  fun cnf skoths (th,ths) =
    1.15    let fun cnf_aux (th,ths) =
    1.16 -  	if has_meta_conn (prop_of th) then ths (*meta-level: ignore*)
    1.17 +  	if not (HOLogic.is_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
    1.18          else if not (has_conns ["All","Ex","op &"] (prop_of th))  
    1.19  	then th::ths (*no work to do, terminate*)
    1.20  	else case head_of (HOLogic.dest_Trueprop (concl_of th)) of