diff -r c13ca04303de -r 60cf5cf30b81 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Mon Jun 25 00:36:40 2007 +0200
+++ b/src/Pure/tactic.ML	Mon Jun 25 00:36:41 2007 +0200
@@ -75,6 +75,7 @@
   val rotate_tac: int -> int -> tactic
   val defer_tac: int -> tactic
   val filter_prems_tac: (term -> bool) -> int -> tactic
+  val eta_long_tac: int -> tactic
 end;
 
 signature TACTIC =
@@ -559,6 +560,10 @@
        end)
   end;
 
+(*eta long beta normal form*)
+fun eta_long_tac i =
+  PRIMITIVE (Conv.fconv_rule (Conv.goals_conv (fn j => i = j) Thm.eta_long_conversion));
+
 end;
 
 structure BasicTactic: BASIC_TACTIC = Tactic;