# HG changeset patch
# User paulson
# Date 1176379047 -7200
# Node ID f10465ee7aa21c3ca2efbbd295a52b795a0cfcfe
# Parent  bc3bb8e9594a9669ac0e020e43243edfd0d0cb2b
Fixed the treatment of TVars in conjecture clauses (they are deleted, not frozen)

diff -r bc3bb8e9594a -r f10465ee7aa2 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Thu Apr 12 13:56:40 2007 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Thu Apr 12 13:57:27 2007 +0200
@@ -29,8 +29,8 @@
 
 (*For running the comparison between combinators and abstractions.
   CANNOT be a ref, as the setting is used while Isabelle is built.
-  Currently FALSE, i.e. all the "abstraction" code below is unused, but so far
-  it seems to be inferior to combinators...*)
+  Currently TRUE: the combinator code cannot be used with proof reconstruction
+  because it is not performed by inference!!*)
 val abstract_lambdas = true;
 
 val trace_abs = ref false;
@@ -608,8 +608,10 @@
 val neg_skolemize_tac = EVERY' [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac];
 
 (*finish_cnf removes tautologies and functional reflexivity axioms, but by calling Thm.varifyT
-  it can introduce TVars, which we don't want in conjecture clauses.*)
-val neg_clausify = map Thm.freezeT o Meson.finish_cnf o assume_abstract_list o make_clauses;
+  it can introduce TVars, which are useless in conjecture clauses.*)
+val no_tvars = null o term_tvars o prop_of;
+
+val neg_clausify = filter no_tvars o Meson.finish_cnf o assume_abstract_list o make_clauses;
 
 fun neg_conjecture_clauses st0 n =
   let val st = Seq.hd (neg_skolemize_tac n st0)