--- a/src/Pure/term.ML Mon Oct 21 20:02:27 2024 +0200
+++ b/src/Pure/term.ML Mon Oct 21 22:28:07 2024 +0200
@@ -183,7 +183,6 @@
val maxidx_term: term -> int -> int
val could_beta_contract: term -> bool
val could_eta_contract: term -> bool
- val could_beta_eta_contract: term -> bool
val used_free: string -> term -> bool
exception USED_FREE of string * term
val dest_abs_fresh: string -> term -> (string * typ) * term
@@ -1045,12 +1044,6 @@
| could_eta_contract (t $ u) = could_eta_contract t orelse could_eta_contract u
| could_eta_contract _ = false;
-fun could_beta_eta_contract (Abs _ $ _) = true
- | could_beta_eta_contract (Abs (_, _, _ $ Bound 0)) = true
- | could_beta_eta_contract (Abs (_, _, b)) = could_beta_eta_contract b
- | could_beta_eta_contract (t $ u) = could_beta_eta_contract t orelse could_beta_eta_contract u
- | could_beta_eta_contract _ = false;
-
(* dest abstraction *)