# HG changeset patch
# User paulson
# Date 1175159523 -7200
# Node ID bd72c625c930525cf3a592cda89ed5dbefa77f67
# Parent  549615dcd4f2d1c61beccc7f1ef97cd1ccd52ed0
Now checks for types-only clause before outputting.

diff -r 549615dcd4f2 -r bd72c625c930 src/HOL/Tools/res_reconstruct.ML
--- 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);