src/HOL/Product_Type.thy
changeset 42411 ff997038e8eb
parent 42284 326f57825e1a
child 43594 ef1ddc59b825
     1.1 --- a/src/HOL/Product_Type.thy	Tue Apr 19 22:32:49 2011 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Tue Apr 19 23:57:28 2011 +0200
     1.3 @@ -336,7 +336,7 @@
     1.4    | strip_abs_split i t =
     1.5        strip_abs_split i (Abs ("x", hd (binder_types (fastype_of t)), t $ Bound 0));
     1.6  
     1.7 -fun let_codegen thy defs dep thyname brack t gr =
     1.8 +fun let_codegen thy mode defs dep thyname brack t gr =
     1.9    (case strip_comb t of
    1.10      (t1 as Const (@{const_name Let}, _), t2 :: t3 :: ts) =>
    1.11      let
    1.12 @@ -347,17 +347,17 @@
    1.13          | dest_let t = ([], t);
    1.14        fun mk_code (l, r) gr =
    1.15          let
    1.16 -          val (pl, gr1) = Codegen.invoke_codegen thy defs dep thyname false l gr;
    1.17 -          val (pr, gr2) = Codegen.invoke_codegen thy defs dep thyname false r gr1;
    1.18 +          val (pl, gr1) = Codegen.invoke_codegen thy mode defs dep thyname false l gr;
    1.19 +          val (pr, gr2) = Codegen.invoke_codegen thy mode defs dep thyname false r gr1;
    1.20          in ((pl, pr), gr2) end
    1.21      in case dest_let (t1 $ t2 $ t3) of
    1.22          ([], _) => NONE
    1.23        | (ps, u) =>
    1.24            let
    1.25              val (qs, gr1) = fold_map mk_code ps gr;
    1.26 -            val (pu, gr2) = Codegen.invoke_codegen thy defs dep thyname false u gr1;
    1.27 +            val (pu, gr2) = Codegen.invoke_codegen thy mode defs dep thyname false u gr1;
    1.28              val (pargs, gr3) = fold_map
    1.29 -              (Codegen.invoke_codegen thy defs dep thyname true) ts gr2
    1.30 +              (Codegen.invoke_codegen thy mode defs dep thyname true) ts gr2
    1.31            in
    1.32              SOME (Codegen.mk_app brack
    1.33                (Pretty.blk (0, [Codegen.str "let ", Pretty.blk (0, flat
    1.34 @@ -370,14 +370,14 @@
    1.35      end
    1.36    | _ => NONE);
    1.37  
    1.38 -fun split_codegen thy defs dep thyname brack t gr = (case strip_comb t of
    1.39 +fun split_codegen thy mode defs dep thyname brack t gr = (case strip_comb t of
    1.40      (t1 as Const (@{const_name prod_case}, _), t2 :: ts) =>
    1.41        let
    1.42          val ([p], u) = strip_abs_split 1 (t1 $ t2);
    1.43 -        val (q, gr1) = Codegen.invoke_codegen thy defs dep thyname false p gr;
    1.44 -        val (pu, gr2) = Codegen.invoke_codegen thy defs dep thyname false u gr1;
    1.45 +        val (q, gr1) = Codegen.invoke_codegen thy mode defs dep thyname false p gr;
    1.46 +        val (pu, gr2) = Codegen.invoke_codegen thy mode defs dep thyname false u gr1;
    1.47          val (pargs, gr3) = fold_map
    1.48 -          (Codegen.invoke_codegen thy defs dep thyname true) ts gr2
    1.49 +          (Codegen.invoke_codegen thy mode defs dep thyname true) ts gr2
    1.50        in
    1.51          SOME (Codegen.mk_app brack
    1.52            (Pretty.block [Codegen.str "(fn ", q, Codegen.str " =>",