list_of_indset now also generates code for set type.
authorberghofe
Tue Dec 13 10:39:32 2005 +0100 (2005-12-13)
changeset 18388ab1a710a68ce
parent 18387 90b2b2fd3fdf
child 18389 8352b1d3b639
list_of_indset now also generates code for set type.
src/HOL/Tools/inductive_codegen.ML
     1.1 --- a/src/HOL/Tools/inductive_codegen.ML	Mon Dec 12 17:24:06 2005 +0100
     1.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Tue Dec 13 10:39:32 2005 +0100
     1.3 @@ -654,9 +654,11 @@
     1.4             val (modes, factors) = lookup_modes gr1 dep;
     1.5             val mode = find_mode gr1 dep s u modes [];
     1.6             val (gr2, ps) =
     1.7 -             compile_expr thy defs dep module false (gr1, (mode, u))
     1.8 +             compile_expr thy defs dep module false (gr1, (mode, u));
     1.9 +           val (gr3, _) =
    1.10 +             invoke_tycodegen thy defs dep module false (gr2, body_type T)
    1.11           in
    1.12 -           SOME (gr2, (if brack then parens else I)
    1.13 +           SOME (gr3, (if brack then parens else I)
    1.14               (Pretty.block ([Pretty.str "Seq.list_of", Pretty.brk 1,
    1.15                 Pretty.str "("] @
    1.16                  conv_ntuple' (snd (valOf (AList.lookup (op =) factors s)))