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)));