# HG changeset patch
# User wenzelm
# Date 1230678494 -3600
# Node ID 6aefc5ff8e6379c36ae690052d8cb17643533aff
# Parent  8615b4f540477f4f94e628f4a0ea12cbdf2c64c2
use exists_subterm directly;
moved old add_term_vars, add_term_frees etc. to structure OldTerm;

diff -r 8615b4f54047 -r 6aefc5ff8e63 src/HOL/Tools/res_reconstruct.ML
--- a/src/HOL/Tools/res_reconstruct.ML	Wed Dec 31 00:08:13 2008 +0100
+++ b/src/HOL/Tools/res_reconstruct.ML	Wed Dec 31 00:08:14 2008 +0100
@@ -1,7 +1,4 @@
-(*  ID:         $Id$
-    Author:     L C Paulson and Claire Quigley
-    Copyright   2004  University of Cambridge
-*)
+(*  Author:     L C Paulson and Claire Quigley, Cambridge University Computer Laboratory *)
 
 (***************************************************************************)
 (*  Code to deal with the transfer of proofs from a prover process         *)
@@ -243,7 +240,7 @@
     singleton (Syntax.check_terms ctxt) (TypeInfer.constrain HOLogic.boolT (fix_sorts vt dt))
   end;
 
-fun gen_all_vars t = fold_rev Logic.all (term_vars t) t;
+fun gen_all_vars t = fold_rev Logic.all (OldTerm.term_vars t) t;
 
 fun ints_of_stree_aux (Int n, ns) = n::ns
   | ints_of_stree_aux (Br(_,ts), ns) = foldl ints_of_stree_aux ns ts;
@@ -253,7 +250,7 @@
 fun decode_tstp vt0 (name, role, ts, annots) ctxt =
   let val deps = case annots of NONE => [] | SOME (source,_) => ints_of_stree source
       val cl = clause_of_strees ctxt vt0 ts
-  in  ((name, role, cl, deps), fold Variable.declare_term (term_frees cl) ctxt)  end;
+  in  ((name, role, cl, deps), fold Variable.declare_term (OldTerm.term_frees cl) ctxt)  end;
 
 fun dest_tstp ((((name, role), ts), annots), chs) =
   case chs of
@@ -409,7 +406,7 @@
       (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
-         exists bad_free (term_frees 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))   
       then (nlines+1, map (replace_deps (lno, deps)) lines) (*Delete line*)