# HG changeset patch
# User wenzelm
# Date 1182724599 -7200
# Node ID 1dfbfc92017ab0591cd6ef05e51b5538e58f98fb
# Parent  6c2156c478f63bcc7d61af5b2539508cb80c6457
made type conv pervasive;
removed obsolete eta_conv (cf. Thm.eta_long_conv);

diff -r 6c2156c478f6 -r 1dfbfc92017a src/Pure/conv.ML
--- a/src/Pure/conv.ML	Mon Jun 25 00:36:38 2007 +0200
+++ b/src/Pure/conv.ML	Mon Jun 25 00:36:39 2007 +0200
@@ -8,11 +8,13 @@
 infix 1 then_conv;
 infix 0 else_conv;
 
+type conv = cterm -> thm;
+
 signature CONV =
 sig
-  type conv = cterm -> thm
   val no_conv: conv
   val all_conv: conv
+  val is_refl: thm -> bool
   val then_conv: conv * conv -> conv
   val else_conv: conv * conv -> conv
   val first_conv: conv list -> conv
@@ -32,9 +34,7 @@
   val concl_conv: int -> conv -> conv
   val prems_conv: int -> (int -> conv) -> conv
   val goals_conv: (int -> bool) -> conv -> conv
-  val eta_conv: theory -> conv 
   val fconv_rule: conv -> thm -> thm
-  val is_refl: thm -> bool
 end;
 
 structure Conv: CONV =
@@ -143,11 +143,6 @@
 
 fun goals_conv pred cv = prems_conv ~1 (fn i => if pred i then cv else all_conv);
 
-fun eta_conv thy ct = 
-  let val {t, ...} = rep_cterm ct
-      val ct' = cterm_of thy (Pattern.eta_long [] t)
-  in (symmetric o eta_conversion) ct'
-  end;
+fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
 
-fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
 end;