# HG changeset patch
# User paulson
# Date 1117642799 -7200
# Node ID 9e2f6c0a779d1377346828acf8992355fb565b35
# Parent  629ba53a072f61fb0c5b4749e68ca7bb118310ad
clausification bug fix

diff -r 629ba53a072f -r 9e2f6c0a779d src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Wed Jun 01 14:50:48 2005 +0200
+++ b/src/HOL/Tools/meson.ML	Wed Jun 01 18:19:59 2005 +0200
@@ -160,7 +160,7 @@
 
 (*Convert all suitable free variables to schematic variables, 
   but don't discharge assumptions.*)
-fun generalize th = forall_elim_vars 0 (forall_intr_frees th);
+fun generalize th = Thm.varifyT (forall_elim_vars 0 (forall_intr_frees th));
 
 fun make_cnf skoths th = map generalize (cnf skoths (th, []));
 
diff -r 629ba53a072f -r 9e2f6c0a779d src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Wed Jun 01 14:50:48 2005 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Wed Jun 01 18:19:59 2005 +0200
@@ -187,7 +187,7 @@
 
 (* transform an Isabelle thm into CNF *)
 fun cnf_axiom_aux th =
-    map (zero_var_indexes o Thm.varifyT) 
+    map zero_var_indexes
         (rm_redundant_cls (cnf_rule (transfer_to_Reconstruction th)));