# HG changeset patch
# User wenzelm
# Date 1133560485 -3600
# Node ID 5d24dbd5e93d80cd228cc229c00b8c9545daea54
# Parent  1a2e30b37ed378df4e2c3a9c4697e791adedc381
abs_def: beta/eta contract lhs;

diff -r 1a2e30b37ed3 -r 5d24dbd5e93d src/Pure/drule.ML
--- a/src/Pure/drule.ML	Fri Dec 02 16:43:42 2005 +0100
+++ b/src/Pure/drule.ML	Fri Dec 02 22:54:45 2005 +0100
@@ -720,17 +720,6 @@
 
 val imp_cong' = combination o combination (reflexive implies)
 
-fun abs_def thm =
-  let
-    val (_, cvs) = strip_comb (fst (dest_equals (cprop_of thm)));
-    val thm' = foldr (fn (ct, thm) => Thm.abstract_rule
-      (case term_of ct of Var ((a, _), _) => a | Free (a, _) => a | _ => "x")
-        ct thm) thm cvs
-  in transitive
-    (symmetric (eta_conversion (fst (dest_equals (cprop_of thm'))))) thm'
-  end;
-
-
 local
   val dest_eq = dest_equals o cprop_of
   val rhs_of = snd o dest_eq
@@ -743,6 +732,19 @@
 fun eta_long_conversion ct = transitive (beta_eta_conversion ct)
   (symmetric (beta_eta_conversion (cterm_fun (Pattern.eta_long []) ct)));
 
+val abs_def =
+  let
+    fun contract_lhs th =
+      Thm.transitive (Thm.symmetric (beta_eta_conversion (fst (dest_equals (cprop_of th))))) th;
+    fun abstract cx = Thm.abstract_rule
+      (case Thm.term_of cx of Var ((x, _), _) => x | Free (x, _) => x | _ => "x") cx;
+  in
+    contract_lhs
+    #> `(snd o strip_comb o fst o dest_equals o cprop_of)
+    #-> fold_rev abstract
+    #> contract_lhs
+  end;
+
 (*In [A1,...,An]==>B, rewrite the selected A's only*)
 fun goals_conv pred cv =
   let fun gconv i ct =