# HG changeset patch
# User wenzelm
# Date 1230670031 -3600
# Node ID 4621affa5c795951a085b4888a906ae8e3a207b2
# Parent  bce03c644efb95315131076d8729ef928f62c0ef
canonical Term.add_var_names, Term.add_tvar_namesT;

diff -r bce03c644efb -r 4621affa5c79 src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Tue Dec 30 21:46:48 2008 +0100
+++ b/src/Pure/Proof/reconstruct.ML	Tue Dec 30 21:47:11 2008 +0100
@@ -232,9 +232,6 @@
 
 (**** update list of free variables of constraints ****)
 
-val add_term_ixns = fold_aterms (fn Var (xi, _) => insert (op =) xi | _ => I);
-val add_typ_ixns = fold_atyps (fn TVar (ai, _) => insert (op =) ai | _ => I);
-
 fun upd_constrs env cs =
   let
     val Envir.Envir {asol, iTs, ...} = env;
@@ -242,8 +239,8 @@
       |> Vartab.fold (cons o #1) asol
       |> Vartab.fold (cons o #1) iTs;
     val vran = []
-      |> Vartab.fold (add_term_ixns o #2 o #2) asol
-      |> Vartab.fold (add_typ_ixns o #2 o #2) iTs;
+      |> Vartab.fold (Term.add_var_names o #2 o #2) asol
+      |> Vartab.fold (Term.add_tvar_namesT o #2 o #2) iTs;
     fun check_cs [] = []
       | check_cs ((u, p, vs)::ps) =
           let val vs' = subtract (op =) dom vs;