# HG changeset patch
# User haftmann
# Date 1178827896 -7200
# Node ID 1feef3b54ce1c984888f594e880e349268cbce3c
# Parent  0b53bd36258b908ab1ab22cf26175809b79caa9e
beta/eta conversion after preprocessor

diff -r 0b53bd36258b -r 1feef3b54ce1 src/HOL/Library/EfficientNat.thy
--- a/src/HOL/Library/EfficientNat.thy	Thu May 10 22:11:35 2007 +0200
+++ b/src/HOL/Library/EfficientNat.thy	Thu May 10 22:11:36 2007 +0200
@@ -366,7 +366,8 @@
 fun lift_obj_eq f thy =
   map (fn thm => thm RS @{thm meta_eq_to_obj_eq})
   #> f thy
-  #> map (fn thm => thm RS @{thm eq_reflection});
+  #> map (fn thm => thm RS @{thm eq_reflection})
+  #> map (Conv.fconv_rule Drule.beta_eta_conversion)
 *}
 
 setup {*