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