# HG changeset patch
# User wenzelm
# Date 1436472804 -7200
# Node ID 03a6b1792cd8201f662842b54e7d339add8b87a2
# Parent  6cc14cf3acffdbb2fb19724c5c90a2553d59f719
clarified specific use of inspect_contract: "any Bound variable will do" may render the term invalid for Term.fastype_of1 in inst_subst_tac (see also 7c3757fccf0e);

diff -r 6cc14cf3acff -r 03a6b1792cd8 src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Thu Jul 09 22:08:20 2015 +0200
+++ b/src/Provers/hypsubst.ML	Thu Jul 09 22:13:24 2015 +0200
@@ -61,7 +61,7 @@
 
 (*Simplifier turns Bound variables to special Free variables:
   change it back (any Bound variable will do)*)
-fun contract t =
+fun inspect_contract t =
   (case Envir.eta_contract t of
     Free (a, T) => if Name.is_bound a then Bound 0 else Free (a, T)
   | t' => t');
@@ -84,7 +84,7 @@
   if novars andalso (has_tvars t orelse has_tvars u)
   then raise Match   (*variables in the type!*)
   else
-    (case (contract t, contract u) of
+    (case apply2 inspect_contract (t, u) of
       (Bound i, _) =>
         if loose_bvar1 (u, i) orelse novars andalso has_vars u
         then raise Match
@@ -165,7 +165,7 @@
 
 fun inst_subst_tac ctxt b rl = CSUBGOAL (fn (cBi, i) =>
   case try (Logic.strip_assums_hyp #> hd #>
-      Data.dest_Trueprop #> Data.dest_eq #> apply2 contract) (Thm.term_of cBi) of
+      Data.dest_Trueprop #> Data.dest_eq #> apply2 Envir.eta_contract) (Thm.term_of cBi) of
     SOME (t, t') =>
       let
         val Bi = Thm.term_of cBi;