# HG changeset patch
# User wenzelm
# Date 1011211107 -3600
# Node ID c5739c1431aba50952bad2f4e7602cf3623b3d65
# Parent  3120e338ffae44455e3adb5862aa47264b847736
export beta_eta_conversion;

diff -r 3120e338ffae -r c5739c1431ab src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Wed Jan 16 20:57:02 2002 +0100
+++ b/src/Pure/meta_simplifier.ML	Wed Jan 16 20:58:27 2002 +0100
@@ -39,6 +39,7 @@
   val set_mk_sym        : meta_simpset * (thm -> thm option) -> meta_simpset
   val set_mk_eq_True    : meta_simpset * (thm -> thm option) -> meta_simpset
   val set_termless      : meta_simpset * (term * term -> bool) -> meta_simpset
+  val beta_eta_conversion: cterm -> thm
   val rewrite_cterm: bool * bool * bool ->
     (meta_simpset -> thm -> thm option) -> meta_simpset -> cterm -> thm
   val goals_conv        : (int -> bool) -> (cterm -> thm) -> cterm -> thm