--- 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;