src/HOL/Product_Type.thy
 changeset 42284 326f57825e1a parent 42247 12fe41a92cd5 child 42411 ff997038e8eb
```     1.1 --- a/src/HOL/Product_Type.thy	Fri Apr 08 11:39:45 2011 +0200
1.2 +++ b/src/HOL/Product_Type.thy	Fri Apr 08 13:31:16 2011 +0200
1.3 @@ -199,8 +199,8 @@
1.4    fun split_tr' [Abs (x, T, t as (Abs abs))] =
1.5          (* split (%x y. t) => %(x,y) t *)
1.6          let
1.7 -          val (y, t') = atomic_abs_tr' abs;
1.8 -          val (x', t'') = atomic_abs_tr' (x, T, t');
1.9 +          val (y, t') = Syntax_Trans.atomic_abs_tr' abs;
1.10 +          val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, T, t');
1.11          in
1.12            Syntax.const @{syntax_const "_abs"} \$
1.13              (Syntax.const @{syntax_const "_pattern"} \$ x' \$ y) \$ t''
1.14 @@ -210,7 +210,7 @@
1.15          let
1.16            val Const (@{syntax_const "_abs"}, _) \$
1.17              (Const (@{syntax_const "_pattern"}, _) \$ y \$ z) \$ t' = split_tr' [t];
1.18 -          val (x', t'') = atomic_abs_tr' (x, T, t');
1.19 +          val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, T, t');
1.20          in
1.21            Syntax.const @{syntax_const "_abs"} \$
1.22              (Syntax.const @{syntax_const "_pattern"} \$ x' \$
1.23 @@ -221,7 +221,7 @@
1.24          split_tr' [(split_tr' [t])] (* inner split_tr' creates next pattern *)
1.25      | split_tr' [Const (@{syntax_const "_abs"}, _) \$ x_y \$ Abs abs] =
1.26          (* split (%pttrn z. t) => %(pttrn,z). t *)
1.27 -        let val (z, t) = atomic_abs_tr' abs in
1.28 +        let val (z, t) = Syntax_Trans.atomic_abs_tr' abs in
1.29            Syntax.const @{syntax_const "_abs"} \$
1.30              (Syntax.const @{syntax_const "_pattern"} \$ x_y \$ z) \$ t
1.31          end
1.32 @@ -239,8 +239,8 @@
1.33          | _ =>
1.34            let
1.35              val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
1.36 -            val (y, t') = atomic_abs_tr' ("y", yT, incr_boundvars 1 t \$ Bound 0);
1.37 -            val (x', t'') = atomic_abs_tr' (x, xT, t');
1.38 +            val (y, t') = Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 1 t \$ Bound 0);
1.39 +            val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, xT, t');
1.40            in
1.41              Syntax.const @{syntax_const "_abs"} \$
1.42                (Syntax.const @{syntax_const "_pattern"} \$ x' \$ y) \$ t''
1.43 @@ -251,8 +251,9 @@
1.44          | _ =>
1.45            let
1.46              val (xT :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
1.47 -            val (y, t') = atomic_abs_tr' ("y", yT, incr_boundvars 2 t \$ Bound 1 \$ Bound 0);
1.48 -            val (x', t'') = atomic_abs_tr' ("x", xT, t');
1.49 +            val (y, t') =
1.50 +              Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 2 t \$ Bound 1 \$ Bound 0);
1.51 +            val (x', t'') = Syntax_Trans.atomic_abs_tr' ("x", xT, t');
1.52            in
1.53              Syntax.const @{syntax_const "_abs"} \$
1.54                (Syntax.const @{syntax_const "_pattern"} \$ x' \$ y) \$ t''
1.55 @@ -276,10 +277,10 @@
1.56      | _ => f ts;
1.57    fun contract2 (Q,f) = (Q, contract Q f);
1.58    val pairs =
1.59 -    [Syntax.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"},
1.60 -     Syntax.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"},
1.61 -     Syntax.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"},
1.62 -     Syntax.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}]
1.63 +    [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"},
1.64 +     Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"},
1.65 +     Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"},
1.66 +     Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}]
1.67  in map contract2 pairs end
1.68  *}
1.69
```