author | wenzelm |
Tue, 03 Apr 2012 17:21:33 +0200 | |
changeset 47296 | c82a0b2606a1 |
parent 47295 | b77980afc975 |
child 47310 | 610d9c212376 |
--- 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;