normalize defs (again, cf. 008b7858f3c0);
authorwenzelm
Tue, 03 Apr 2012 17:21:33 +0200
changeset 47296 c82a0b2606a1
parent 47295 b77980afc975
child 47310 610d9c212376
normalize defs (again, cf. 008b7858f3c0);
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;