src/Pure/drule.ML
changeset 52131 366fa32ee2a3
parent 48127 d30957198bbb
child 52223 5bb6ae8acb87
     1.1 --- a/src/Pure/drule.ML	Fri May 24 16:42:57 2013 +0200
     1.2 +++ b/src/Pure/drule.ML	Fri May 24 17:00:46 2013 +0200
     1.3 @@ -470,7 +470,7 @@
     1.4  fun eta_long_conversion ct =
     1.5    Thm.transitive
     1.6      (beta_eta_conversion ct)
     1.7 -    (Thm.symmetric (beta_eta_conversion (cterm_fun (Pattern.eta_long []) ct)));
     1.8 +    (Thm.symmetric (beta_eta_conversion (cterm_fun (Envir.eta_long []) ct)));
     1.9  
    1.10  (*Contract all eta-redexes in the theorem, lest they give rise to needless abstractions*)
    1.11  fun eta_contraction_rule th =