beta/eta conversion after preprocessor
authorhaftmann
Thu May 10 22:11:36 2007 +0200 (2007-05-10)
changeset 229281feef3b54ce1
parent 22927 0b53bd36258b
child 22929 e6b6f8dd03e9
beta/eta conversion after preprocessor
src/HOL/Library/EfficientNat.thy
     1.1 --- a/src/HOL/Library/EfficientNat.thy	Thu May 10 22:11:35 2007 +0200
     1.2 +++ b/src/HOL/Library/EfficientNat.thy	Thu May 10 22:11:36 2007 +0200
     1.3 @@ -366,7 +366,8 @@
     1.4  fun lift_obj_eq f thy =
     1.5    map (fn thm => thm RS @{thm meta_eq_to_obj_eq})
     1.6    #> f thy
     1.7 -  #> map (fn thm => thm RS @{thm eq_reflection});
     1.8 +  #> map (fn thm => thm RS @{thm eq_reflection})
     1.9 +  #> map (Conv.fconv_rule Drule.beta_eta_conversion)
    1.10  *}
    1.11  
    1.12  setup {*