# 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')