# HG changeset patch
# User paulson
# Date 1159802982 -7200
# Node ID 634070b407316ea2c4dc00f038f8343fbb209ba4
# Parent  bae9a1002d84c9a715e4a598233b2a88a2db07da
Now checks explicitly for Trueprop, thereby ignoring junk theorems involving OF_CLASS, etc.

diff -r bae9a1002d84 -r 634070b40731 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Sun Oct 01 22:19:24 2006 +0200
+++ b/src/HOL/Tools/meson.ML	Mon Oct 02 17:29:42 2006 +0200
@@ -203,6 +203,8 @@
   presumably to instantiate a Boolean variable.*)
 fun resop nf [prem] = resolve_tac (nf prem) 1;
 
+(*Any need to extend this list with 
+  "HOL.type_class","OperationalEquality.eq_class","ProtoPure.term"?*)
 val has_meta_conn = 
     exists_Const (fn (c,_) => c mem_string ["==", "==>", "all", "prop"]);
 
@@ -216,7 +218,7 @@
   Eliminates existential quantifiers using skoths: Skolemization theorems.*)
 fun cnf skoths (th,ths) =
   let fun cnf_aux (th,ths) =
-  	if has_meta_conn (prop_of th) then ths (*meta-level: ignore*)
+  	if not (HOLogic.is_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