# HG changeset patch
# User wenzelm
# Date 1183475833 -7200
# Node ID df5440e241a14d37a3b92d4ef362a803e6fa2fb6
# Parent  438e5c4ef2c0b8c7e875d58ddd093fb77c61914a
removed obsolete eta_long_tac;

diff -r 438e5c4ef2c0 -r df5440e241a1 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Tue Jul 03 17:17:13 2007 +0200
+++ b/src/Pure/tactic.ML	Tue Jul 03 17:17:13 2007 +0200
@@ -75,7 +75,6 @@
   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 =
@@ -560,10 +559,6 @@
        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;