# HG changeset patch
# User berghofe
# Date 1026230606 -7200
# Node ID 5b5e12f0aee08b5a893f6a482eccabb5470d732e
# Parent  39d1b3a4c6f41e5ddb96158c94da46431411f878
Added function abs_def.

diff -r 39d1b3a4c6f4 -r 5b5e12f0aee0 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Tue Jul 09 17:25:42 2002 +0200
+++ b/src/Pure/drule.ML	Tue Jul 09 18:03:26 2002 +0200
@@ -130,6 +130,7 @@
   val conj_elim_list: thm -> thm list
   val conj_elim_precise: int -> thm -> thm list
   val conj_intr_thm: thm
+  val abs_def: thm -> thm
 end;
 
 structure Drule: DRULE =
@@ -589,6 +590,16 @@
 
 val refl_implies = 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) (cvs, thm)
+  in transitive
+    (symmetric (eta_conversion (fst (dest_equals (cprop_of thm'))))) thm'
+  end;
+
 
 (*** Some useful meta-theorems ***)