--- a/src/HOL/Tools/code_evaluation.ML Fri Aug 05 20:43:40 2016 +0200
+++ b/src/HOL/Tools/code_evaluation.ML Fri Aug 05 22:15:30 2016 +0200
@@ -152,7 +152,7 @@
end;
fun subst_termify_app (Const (@{const_name termify}, _), [t]) =
- if not (Term.has_abs t)
+ if not (Term.exists_subterm (fn Abs _ => true | _ => false) t)
then if fold_aterms (fn Const _ => I | _ => K false) t true
then SOME (HOLogic.reflect_term t)
else error "Cannot termify expression containing variable"
--- a/src/Pure/envir.ML Fri Aug 05 20:43:40 2016 +0200
+++ b/src/Pure/envir.ML Fri Aug 05 22:15:30 2016 +0200
@@ -221,7 +221,9 @@
else norm_term2 envir;
fun norm_term envir t = norm_term_same envir t handle Same.SAME => t;
-fun beta_norm t = if Term.has_abs t then norm_term init t else t;
+
+fun beta_norm t =
+ if Term.could_beta_contract t then norm_term init t else t;
end;
@@ -289,7 +291,7 @@
in
fun eta_contract t =
- if Term.has_abs t then Same.commit eta t else t;
+ if Term.could_eta_contract t then Same.commit eta t else t;
end;
--- a/src/Pure/term.ML Fri Aug 05 20:43:40 2016 +0200
+++ b/src/Pure/term.ML Fri Aug 05 22:15:30 2016 +0200
@@ -160,7 +160,9 @@
val maxidx_typ: typ -> int -> int
val maxidx_typs: typ list -> int -> int
val maxidx_term: term -> int -> int
- val has_abs: term -> bool
+ val could_beta_contract: term -> bool
+ val could_eta_contract: term -> bool
+ val could_beta_eta_contract: term -> bool
val dest_abs: string * typ * term -> string * term
val dummy_pattern: typ -> term
val dummy: term
@@ -913,9 +915,24 @@
fun exists_Const P = exists_subterm (fn Const c => P c | _ => false);
-fun has_abs (Abs _) = true
- | has_abs (t $ u) = has_abs t orelse has_abs u
- | has_abs _ = false;
+
+(* contraction *)
+
+fun could_beta_contract (Abs _ $ _) = true
+ | could_beta_contract (t $ u) = could_beta_contract t orelse could_beta_contract u
+ | could_beta_contract (Abs (_, _, b)) = could_beta_contract b
+ | could_beta_contract _ = false;
+
+fun could_eta_contract (Abs (_, _, _ $ Bound 0)) = true
+ | could_eta_contract (Abs (_, _, b)) = could_eta_contract b
+ | 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 *)