# HG changeset patch
# User paulson
# Date 1192721667 -7200
# Node ID 729f9aad1f504dafb1cc13e4c533f21762ad238d
# Parent  aa9db4e3cd5e7c518cb52d16119a3ef329336236
Improving the propagation of type constraints for Frees

diff -r aa9db4e3cd5e -r 729f9aad1f50 src/HOL/Tools/res_reconstruct.ML
--- a/src/HOL/Tools/res_reconstruct.ML	Thu Oct 18 17:33:57 2007 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML	Thu Oct 18 17:34:27 2007 +0200
@@ -253,9 +253,10 @@
 
 fun ints_of_stree t = ints_of_stree_aux (t, []);
 
-fun decode_tstp ctxt vt0 (name, role, ts, annots) =
+fun decode_tstp vt0 (name, role, ts, annots) ctxt =
   let val deps = case annots of NONE => [] | SOME (source,_) => ints_of_stree source
-  in  (name, role, clause_of_strees ctxt vt0 ts, deps)  end;
+      val cl = clause_of_strees ctxt vt0 ts
+  in  ((name, role, cl, deps), fold Variable.declare_term (term_frees cl) ctxt)  end;
 
 fun dest_tstp ((((name, role), ts), annots), chs) =
   case chs of
@@ -280,7 +281,7 @@
 
 fun decode_tstp_list ctxt tuples =
   let val vt0 = tfree_constraints_of_clauses Vartab.empty (map #3 tuples)
-  in  map (decode_tstp ctxt vt0) tuples  end;
+  in  #1 (fold_map (decode_tstp vt0) tuples ctxt) end;
 
 (** Finding a matching assumption. The literals may be permuted, and variable names
     may disagree. We have to try all combinations of literals (quadratic!) and