src/Pure/Isar/local_defs.ML

--- a/src/Pure/Isar/local_defs.ML	Tue Apr 03 16:53:32 2012 +0200
+++ b/src/Pure/Isar/local_defs.ML	Tue Apr 03 17:21:33 2012 +0200
@@ -149,7 +149,7 @@
                   NONE => (asm, false)
                 | SOME u =>
                     if t aconv u then (asm, false)
-                    else (Drule.abs_def asm, true))
+                    else (Drule.abs_def (Drule.gen_all asm), true))
               end)));
       in (pairself (map #1) (List.partition #2 defs_asms), th') end
   end;