# HG changeset patch # User dixon # Date 1109094142 -3600 # Node ID 0efa7126003ffa6075a08effc864007cc2caaebe # Parent 5f3ef1ddda1fef53992a80e653928c75397a46d2 Lucas - fixed bug in zero_var_indexes: it was ignoring vars in the flex-flex pairs. These are now taken into account. diff -r 5f3ef1ddda1f -r 0efa7126003f src/Pure/drule.ML --- a/src/Pure/drule.ML Tue Feb 22 13:05:47 2005 +0100 +++ b/src/Pure/drule.ML Tue Feb 22 18:42:22 2005 +0100 @@ -362,10 +362,14 @@ (*Reset Var indexes to zero, renaming to preserve distinctness*) fun zero_var_indexes th = - let val {prop,sign,...} = rep_thm th; - val vars = term_vars prop + let val {prop,sign,tpairs,...} = rep_thm th; + val (tpair_l, tpair_r) = Library.split_list tpairs; + val vars = foldr add_term_vars + (tpair_r, foldr add_term_vars (tpair_l, (term_vars prop))); val bs = foldl add_new_id ([], map (fn Var((a,_),_)=>a) vars) - val inrs = add_term_tvars(prop,[]); + val inrs = + foldr add_term_tvars + (tpair_r, foldr add_term_tvars (tpair_l, (term_tvars prop))); val nms' = rev(foldl add_new_id ([], map (#1 o #1) inrs)); val tye = ListPair.map (fn ((v,rs),a) => (v, TVar((a,0),rs))) (inrs, nms')