# HG changeset patch
# User wenzelm
# Date 1333466493 -7200
# Node ID c82a0b2606a128980fb8fcea43bcd4c4dabc0d22
# Parent  b77980afc975e5789efd0634891522b7e65d523d
normalize defs (again, cf. 008b7858f3c0);

diff -r b77980afc975 -r c82a0b2606a1 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;