diff -r 1d685baea08e -r fb3ccf499df5 src/HOL/Tools/res_reconstruct.ML
--- a/src/HOL/Tools/res_reconstruct.ML	Wed Dec 31 18:53:16 2008 +0100
+++ b/src/HOL/Tools/res_reconstruct.ML	Wed Dec 31 18:53:17 2008 +0100
@@ -405,7 +405,7 @@
 fun add_wanted_prfline ctxt ((lno, t, []), (nlines, lines)) =
       (nlines, (lno, t, []) :: lines)   (*conjecture clauses must be kept*)
   | add_wanted_prfline ctxt ((lno, t, deps), (nlines, lines)) =
-      if eq_types t orelse not (null (term_tvars t)) orelse
+      if eq_types t orelse not (null (Term.add_tvars t [])) orelse
          exists_subterm bad_free t orelse
          (not (null lines) andalso   (*final line can't be deleted for these reasons*)
           (length deps < 2 orelse nlines mod (Config.get ctxt modulus) <> 0))