src/HOL/Product_Type.thy
changeset 30604 2a9911f4b0a3
parent 28719 01e04e41cc7b
child 30924 c1ed09f3fbfe
     1.1 --- a/src/HOL/Product_Type.thy	Thu Mar 19 08:13:10 2009 -0700
     1.2 +++ b/src/HOL/Product_Type.thy	Fri Mar 20 10:43:53 2009 +0100
     1.3 @@ -981,7 +981,8 @@
     1.4    | strip_abs_split i (u as Const ("split", _) $ t) = (case strip_abs_split (i+1) t of
     1.5          (v :: v' :: vs, u) => (HOLogic.mk_prod (v, v') :: vs, u)
     1.6        | _ => ([], u))
     1.7 -  | strip_abs_split i t = ([], t);
     1.8 +  | strip_abs_split i t =
     1.9 +      strip_abs_split i (Abs ("x", hd (binder_types (fastype_of t)), t $ Bound 0));
    1.10  
    1.11  fun let_codegen thy defs dep thyname brack t gr = (case strip_comb t of
    1.12      (t1 as Const ("Let", _), t2 :: t3 :: ts) =>
    1.13 @@ -1018,19 +1019,17 @@
    1.14  
    1.15  fun split_codegen thy defs dep thyname brack t gr = (case strip_comb t of
    1.16      (t1 as Const ("split", _), t2 :: ts) =>
    1.17 -      (case strip_abs_split 1 (t1 $ t2) of
    1.18 -         ([p], u) =>
    1.19 -           let
    1.20 -             val (q, gr1) = Codegen.invoke_codegen thy defs dep thyname false p gr;
    1.21 -             val (pu, gr2) = Codegen.invoke_codegen thy defs dep thyname false u gr1;
    1.22 -             val (pargs, gr3) = fold_map
    1.23 -               (Codegen.invoke_codegen thy defs dep thyname true) ts gr2
    1.24 -           in
    1.25 -             SOME (Codegen.mk_app brack
    1.26 -               (Pretty.block [Codegen.str "(fn ", q, Codegen.str " =>",
    1.27 -                 Pretty.brk 1, pu, Codegen.str ")"]) pargs, gr2)
    1.28 -           end
    1.29 -       | _ => NONE)
    1.30 +      let
    1.31 +        val ([p], u) = strip_abs_split 1 (t1 $ t2);
    1.32 +        val (q, gr1) = Codegen.invoke_codegen thy defs dep thyname false p gr;
    1.33 +        val (pu, gr2) = Codegen.invoke_codegen thy defs dep thyname false u gr1;
    1.34 +        val (pargs, gr3) = fold_map
    1.35 +          (Codegen.invoke_codegen thy defs dep thyname true) ts gr2
    1.36 +      in
    1.37 +        SOME (Codegen.mk_app brack
    1.38 +          (Pretty.block [Codegen.str "(fn ", q, Codegen.str " =>",
    1.39 +            Pretty.brk 1, pu, Codegen.str ")"]) pargs, gr2)
    1.40 +      end
    1.41    | _ => NONE);
    1.42  
    1.43  in