src/HOL/Tools/inductive_codegen.ML
changeset 31852 a16bb835e97d
parent 31784 bd3486c57ba3
child 31998 2c7a24f74db9
     1.1 --- a/src/HOL/Tools/inductive_codegen.ML	Mon Jun 29 12:18:57 2009 +0200
     1.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Mon Jun 29 12:18:57 2009 +0200
     1.3 @@ -378,7 +378,7 @@
     1.4            end
     1.5        | compile_prems out_ts vs names ps gr =
     1.6            let
     1.7 -            val vs' = distinct (op =) (List.concat (vs :: map term_vs out_ts));
     1.8 +            val vs' = distinct (op =) (flat (vs :: map term_vs out_ts));
     1.9              val SOME (p, mode as SOME (Mode (_, js, _))) =
    1.10                select_mode_prem thy modes' vs' ps;
    1.11              val ps' = filter_out (equal p) ps;
    1.12 @@ -404,7 +404,9 @@
    1.13                           (compile_expr thy defs dep module false modes
    1.14                             (mode, t) gr2)
    1.15                       else
    1.16 -                       apfst (fn p => [str "DSeq.of_list", Pretty.brk 1, p])
    1.17 +                       apfst (fn p => Pretty.breaks [str "DSeq.of_list", str "(case", p,
    1.18 +                         str "of", str "Set", str "xs", str "=>", str "xs)"])
    1.19 +                         (*this is a very strong assumption about the generated code!*)
    1.20                             (invoke_codegen thy defs dep module true t gr2);
    1.21                     val (rest, gr4) = compile_prems out_ts''' vs' (fst nvs) ps' gr3;
    1.22                   in
    1.23 @@ -661,8 +663,10 @@
    1.24                      let val (call_p, gr') = mk_ind_call thy defs dep module true
    1.25                        s T (ts1 @ ts2') names thyname k intrs gr 
    1.26                      in SOME ((if brack then parens else I) (Pretty.block
    1.27 -                      [str "DSeq.list_of", Pretty.brk 1, str "(",
    1.28 -                       conv_ntuple fs ots call_p, str ")"]), gr')
    1.29 +                      [str "Set", Pretty.brk 1, str "(DSeq.list_of", Pretty.brk 1, str "(",
    1.30 +                       conv_ntuple fs ots call_p, str "))"]),
    1.31 +                       (*this is a very strong assumption about the generated code!*)
    1.32 +                       gr')
    1.33                      end
    1.34                    else NONE
    1.35                  end