# HG changeset patch
# User wenzelm
# Date 1182724602 -7200
# Node ID a056eefb76e556f7426662e7aa869b8bdd9cb21a
# Parent  60cf5cf30b8121f2e3bf7f1cbd54db18c103ada5
added eta_long_conversion;

diff -r 60cf5cf30b81 -r a056eefb76e5 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Mon Jun 25 00:36:41 2007 +0200
+++ b/src/Pure/thm.ML	Mon Jun 25 00:36:42 2007 +0200
@@ -90,6 +90,7 @@
   val transitive: thm -> thm -> thm
   val beta_conversion: bool -> cterm -> thm
   val eta_conversion: cterm -> thm
+  val eta_long_conversion: cterm -> thm
   val abstract_rule: string -> cterm -> thm -> thm
   val combination: thm -> thm -> thm
   val equal_intr: thm -> thm -> thm
@@ -813,6 +814,16 @@
     tpairs = [],
     prop = Logic.mk_equals (t, Envir.eta_contract t)};
 
+fun eta_long_conversion (Cterm {thy_ref, t, T, maxidx, sorts}) =
+  Thm {thy_ref = thy_ref,
+    der = Pt.infer_derivs' I (false, Pt.reflexive),
+    tags = [],
+    maxidx = maxidx,
+    shyps = sorts,
+    hyps = [],
+    tpairs = [],
+    prop = Logic.mk_equals (t, Pattern.eta_long [] t)};
+
 (*The abstraction rule.  The Free or Var x must not be free in the hypotheses.
   The bound variable will be named "a" (since x will be something like x320)
       t == u