src/Pure/Isar/local_defs.ML

--- a/src/Pure/Isar/local_defs.ML	Sat Mar 07 15:40:36 2015 +0100
+++ b/src/Pure/Isar/local_defs.ML	Sat Mar 07 21:32:31 2015 +0100
@@ -147,7 +147,7 @@
                   NONE => (asm, false)
                 | SOME u =>
                     if t aconv u then (asm, false)
-                    else (Drule.abs_def (Drule.gen_all asm), true))
+                    else (Drule.abs_def (Drule.gen_all (Variable.maxidx_of outer) asm), true))
               end)));
       in (apply2 (map #1) (List.partition #2 defs_asms), th') end
   end;