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