# HG changeset patch
# User dixon
# Date 1109755990 -3600
# Node ID c862d556fb189d9e62df044e391201036dbf91ab
# Parent  10c5c689aa20933633c352eecbd9b09a60a58534
lucas - fixed bug with name capture variables bound outside redex could (previously)conflict with scheme variables that occur in the conditions of an equation, and which were renamed to avoid conflict with another instantiation. This has now been fixed.

diff -r 10c5c689aa20 -r c862d556fb18 src/Pure/IsaPlanner/rw_inst.ML
--- a/src/Pure/IsaPlanner/rw_inst.ML	Wed Mar 02 10:21:17 2005 +0100
+++ b/src/Pure/IsaPlanner/rw_inst.ML	Wed Mar 02 10:33:10 2005 +0100
@@ -88,23 +88,26 @@
          bound vars with binders outside the redex *)
       val prop = Thm.prop_of rule;
       val names = Term.add_term_names (prop, []);
-      val (fromnames,tonames,names2) = 
-          foldl (fn ((rnf,rnt,names),(n,ty)) => 
+      val (fromnames,tonames,names2,Ts') = 
+          foldl (fn ((rnf,rnt,names, Ts'),(n,ty)) => 
                     let val n2 = Term.variant names n in
                       (ctermify (Free(RWTools.mk_fake_bound_name n,
                                       ty)) :: rnf,
                        ctermify (Free(n2,ty)) :: rnt, 
-                       n2 :: names)
+                       n2 :: names,
+                       (n2,ty) :: Ts')
                     end)
-                (([],[],names), Ts);
+                (([],[],names, []), Ts);
+
       val rule' = rule |> Drule.forall_intr_list fromnames
                        |> Drule.forall_elim_list tonames;
       
       (* make unconditional rule and prems *)
-      val (uncond_rule, cprems) = IsaND.allify_conditions ctermify Ts rule';
+      val (uncond_rule, cprems) = IsaND.allify_conditions ctermify (rev Ts') 
+                                                          rule';
 
       (* using these names create lambda-abstracted version of the rule *)
-      val abstractions = Ts ~~ (rev tonames);
+      val abstractions = rev (Ts' ~~ tonames);
       val abstract_rule = foldl (fn (th,((n,ty),ct)) => 
                                     Thm.abstract_rule n ct th)
                                 (uncond_rule, abstractions);