src/HOL/Tools/res_axioms.ML

--- a/src/HOL/Tools/res_axioms.ML	Sat Mar 12 00:07:05 2005 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Mon Mar 14 17:04:10 2005 +0100
@@ -262,7 +262,7 @@
     let val thm' = transfer_to_Reconstruction thm
 	val thm'' = if (is_elimR thm') then (cnf_elim thm')  else cnf_rule thm'
     in
-	rm_redundant_cls thm''
+	map Thm.varifyT (rm_redundant_cls thm'')
     end;
 
 fun meta_cnf_axiom thm =