src/HOL/Product_Type.thy
changeset 42083 e1209fc7ecdc
parent 42059 83f3dc509068
child 42247 12fe41a92cd5
     1.1 --- a/src/HOL/Product_Type.thy	Thu Mar 24 16:47:24 2011 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Thu Mar 24 16:56:19 2011 +0100
     1.3 @@ -272,7 +272,7 @@
     1.4    fun contract Q f ts =
     1.5      case ts of
     1.6        [A, Abs(_, _, (s as Const (@{const_syntax prod_case},_) $ t) $ Bound 0)]
     1.7 -      => if loose_bvar1 (t,0) then f ts else Syntax.const Q $ A $ s
     1.8 +      => if Term.is_dependent t then f ts else Syntax.const Q $ A $ s
     1.9      | _ => f ts;
    1.10    fun contract2 (Q,f) = (Q, contract Q f);
    1.11    val pairs =