Now checks for types-only clause before outputting.

--- a/src/HOL/Tools/res_reconstruct.ML	Wed Mar 28 19:18:39 2007 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML	Thu Mar 29 11:12:03 2007 +0200
@@ -424,7 +424,8 @@
       (nlines, (lno, t, []) :: lines)   (*conjecture clauses must be kept*)
   | add_wanted_prfline (line, (nlines, [])) = (nlines, [line])   (*final line must be kept*)
   | add_wanted_prfline ((lno, t, deps), (nlines, lines)) =
-      if not (null (term_tvars t)) orelse length deps < 2 orelse nlines mod !modulus <> 0
+      if eq_types t orelse not (null (term_tvars t)) orelse
+         length deps < 2 orelse nlines mod !modulus <> 0
       then (nlines+1, map (replace_deps (lno, deps)) lines) (*Delete line*)
       else (nlines+1, (lno, t, deps) :: lines);