src/Pure/Tools/codegen_package.ML
changeset 20976 e324808e9f1f
parent 20931 19d9b78218fd
child 21012 f08574148b7a
     1.1 --- a/src/Pure/Tools/codegen_package.ML	Wed Oct 11 14:51:41 2006 +0200
     1.2 +++ b/src/Pure/Tools/codegen_package.ML	Wed Oct 11 20:35:54 2006 +0200
     1.3 @@ -417,10 +417,31 @@
     1.4  fun appgen_case dest_case_expr thy algbr funcgr strct (app as (c_ty, ts)) trns =
     1.5    let
     1.6      val SOME ([], ((st, sty), ds)) = dest_case_expr thy (list_comb (Const c_ty, ts));
     1.7 -    fun clausegen (dt, bt) trns =
     1.8 -      trns
     1.9 -      |> exprgen_term thy algbr funcgr strct dt
    1.10 -      ||>> exprgen_term thy algbr funcgr strct bt;
    1.11 +    fun fold_map_aterms f (t $ u) s =
    1.12 +          s
    1.13 +          |> fold_map_aterms f t
    1.14 +          ||>> fold_map_aterms f u
    1.15 +          |-> (fn (t1, t2) => pair (t1 $ t2))
    1.16 +      | fold_map_aterms f (Abs (v, ty, t)) s =
    1.17 +          s
    1.18 +          |> fold_map_aterms f t
    1.19 +          |-> (fn t' => pair (Abs (v, ty, t')))
    1.20 +      | fold_map_aterms f a s = f a s;
    1.21 +    fun purify_term_frees (Free (v, ty)) ctxt = 
    1.22 +          let
    1.23 +            val ([v'], ctxt') = Name.variants [CodegenNames.purify_var v] ctxt;
    1.24 +          in (Free (v, ty), ctxt') end
    1.25 +      | purify_term_frees t ctxt = (t, ctxt);
    1.26 +    fun clausegen (raw_dt, raw_bt) trns =
    1.27 +      let
    1.28 +        val ((dt, bt), _) = Name.context
    1.29 +          |> fold_map_aterms purify_term_frees raw_dt
    1.30 +          ||>> fold_map_aterms purify_term_frees raw_bt;
    1.31 +      in
    1.32 +        trns
    1.33 +        |> exprgen_term thy algbr funcgr strct dt
    1.34 +        ||>> exprgen_term thy algbr funcgr strct bt
    1.35 +      end;
    1.36    in
    1.37      trns
    1.38      |> exprgen_term thy algbr funcgr strct st