# HG changeset patch
# User huffman
# Date 1274558193 25200
# Node ID 3e5146b93218255d50708f6ec5296483155e9904
# Parent  a2a1c8a658ef85daf81eef8cbc08c6b9e8d2d046
simplify definition of eta_tac

diff -r a2a1c8a658ef -r 3e5146b93218 src/HOLCF/Tools/fixrec.ML
--- a/src/HOLCF/Tools/fixrec.ML	Sat May 22 12:36:50 2010 -0700
+++ b/src/HOLCF/Tools/fixrec.ML	Sat May 22 12:56:33 2010 -0700
@@ -302,9 +302,7 @@
 (********************** Proving associated theorems **********************)
 (*************************************************************************)
 
-(* tactic to perform eta-contraction on subgoal *)
-fun eta_tac (ctxt : Proof.context) : int -> tactic =
-  EqSubst.eqsubst_tac ctxt [0] @{thms refl};
+fun eta_tac i = CONVERSION Thm.eta_conversion i;
 
 fun fixrec_simp_tac ctxt =
   let
@@ -320,7 +318,7 @@
         val unfold_thm = the (Symtab.lookup tab c);
         val rule = unfold_thm RS @{thm ssubst_lhs};
       in
-        CHANGED (rtac rule i THEN eta_tac ctxt i THEN asm_simp_tac ss i)
+        CHANGED (rtac rule i THEN eta_tac i THEN asm_simp_tac ss i)
       end
   in
     SUBGOAL (fn ti => the_default no_tac (try tac ti))
@@ -331,7 +329,7 @@
   let
     val ss = Simplifier.simpset_of ctxt;
     val rule = unfold_thm RS @{thm ssubst_lhs};
-    val tac = rtac rule 1 THEN eta_tac ctxt 1 THEN asm_simp_tac ss 1;
+    val tac = rtac rule 1 THEN eta_tac 1 THEN asm_simp_tac ss 1;
     fun prove_term t = Goal.prove ctxt [] [] t (K tac);
     fun prove_eqn (bind, eqn_t) = (bind, prove_term eqn_t);
   in