src/HOL/Product_Type.thy
changeset 42083 e1209fc7ecdc
parent 42059 83f3dc509068
child 42247 12fe41a92cd5
equal deleted inserted replaced
42082:47f8bfe0f597 42083:e1209fc7ecdc
   270 print_translation {*
   270 print_translation {*
   271 let
   271 let
   272   fun contract Q f ts =
   272   fun contract Q f ts =
   273     case ts of
   273     case ts of
   274       [A, Abs(_, _, (s as Const (@{const_syntax prod_case},_) $ t) $ Bound 0)]
   274       [A, Abs(_, _, (s as Const (@{const_syntax prod_case},_) $ t) $ Bound 0)]
   275       => if loose_bvar1 (t,0) then f ts else Syntax.const Q $ A $ s
   275       => if Term.is_dependent t then f ts else Syntax.const Q $ A $ s
   276     | _ => f ts;
   276     | _ => f ts;
   277   fun contract2 (Q,f) = (Q, contract Q f);
   277   fun contract2 (Q,f) = (Q, contract Q f);
   278   val pairs =
   278   val pairs =
   279     [Syntax.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"},
   279     [Syntax.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"},
   280      Syntax.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"},
   280      Syntax.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"},