# HG changeset patch
# User berghofe
# Date 1134466772 -3600
# Node ID ab1a710a68cee028a92f7b2044d7ff54fb218321
# Parent  90b2b2fd3fdf61a53f8f008df0b72a3cfe9b3c72
list_of_indset now also generates code for set type.

diff -r 90b2b2fd3fdf -r ab1a710a68ce 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)))