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.

--- 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);