--- a/src/Pure/drule.ML Wed May 04 10:44:53 2005 +0200
+++ b/src/Pure/drule.ML Wed May 04 18:50:21 2005 +0200
@@ -115,6 +115,7 @@
val merge_rules: thm list * thm list -> thm list
val imp_cong' : thm -> thm -> thm
val beta_eta_conversion: cterm -> thm
+ val eta_long_conversion: cterm -> thm
val goals_conv : (int -> bool) -> (cterm -> thm) -> cterm -> thm
val forall_conv : (cterm -> thm) -> cterm -> thm
val fconv_rule : (cterm -> thm) -> thm -> thm
@@ -698,6 +699,9 @@
in transitive thm (eta_conversion (rhs_of thm)) end
end;
+fun eta_long_conversion ct = transitive (beta_eta_conversion ct)
+ (symmetric (beta_eta_conversion (cterm_fun (Pattern.eta_long []) ct)));
+
(*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*)
fun goals_conv pred cv =
let fun gconv i ct =