1.1 --- a/src/Pure/meta_simplifier.ML	Wed Jan 16 20:57:02 2002 +0100
     1.2 +++ b/src/Pure/meta_simplifier.ML	Wed Jan 16 20:58:27 2002 +0100
     1.3 @@ -39,6 +39,7 @@
     1.4    val set_mk_sym        : meta_simpset * (thm -> thm option) -> meta_simpset
     1.5    val set_mk_eq_True    : meta_simpset * (thm -> thm option) -> meta_simpset
     1.6    val set_termless      : meta_simpset * (term * term -> bool) -> meta_simpset
     1.7 +  val beta_eta_conversion: cterm -> thm
     1.8    val rewrite_cterm: bool * bool * bool ->
     1.9      (meta_simpset -> thm -> thm option) -> meta_simpset -> cterm -> thm
    1.10    val goals_conv        : (int -> bool) -> (cterm -> thm) -> cterm -> thm