# HG changeset patch
# User wenzelm
# Date 1433016255 -7200
# Node ID e487b83a9885f95ef5dd99fb5bc2ef934497fd02
# Parent  c08adefc98ea3d5bba958c603f84cbb8206e2490
tuned;

diff -r c08adefc98ea -r e487b83a9885 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Sat May 30 21:52:37 2015 +0200
+++ b/src/Pure/drule.ML	Sat May 30 22:04:15 2015 +0200
@@ -431,14 +431,9 @@
 fun fun_cong_rule th ct = Thm.combination th (Thm.reflexive ct);    (*AP_THM in LCF/HOL*)
 fun binop_cong_rule ct th1 th2 = Thm.combination (arg_cong_rule ct th1) th2;
 
-local
-  val dest_eq = Thm.dest_equals o Thm.cprop_of
-  val rhs_of = snd o dest_eq
-in
-fun beta_eta_conversion t =
-  let val thm = Thm.beta_conversion true t
-  in Thm.transitive thm (Thm.eta_conversion (rhs_of thm)) end
-end;
+fun beta_eta_conversion ct =
+  let val thm = Thm.beta_conversion true ct
+  in Thm.transitive thm (Thm.eta_conversion (Thm.rhs_of thm)) end;
 
 fun eta_long_conversion ct =
   Thm.transitive