# HG changeset patch
# User wenzelm
# Date 1470428130 -7200
# Node ID 9c870388e87aea26845ad40675fef2783cc02b8a
# Parent  9c4bb72d1f4f2af17fa3d7bb87d0814afd1eb747
more tight filtering;

diff -r 9c4bb72d1f4f -r 9c870388e87a src/HOL/Tools/code_evaluation.ML
--- 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"
diff -r 9c4bb72d1f4f -r 9c870388e87a src/Pure/envir.ML
--- 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;
 
diff -r 9c4bb72d1f4f -r 9c870388e87a src/Pure/term.ML
--- 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 *)