# HG changeset patch
# User berghofe
# Date 1158928583 -7200
# Node ID 0e4df994ad348628b6065a8f48bd956e9f3d9792
# Parent  fd92d9310128c0b7878b79e85d5e66fe7ee5dda2
Fixed bug concerning the generation of identifiers for
datatypes, which caused the code generator to fail for
mutually recursive datatypes.

diff -r fd92d9310128 -r 0e4df994ad34 src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Fri Sep 22 14:32:46 2006 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML	Fri Sep 22 14:36:23 2006 +0200
@@ -200,7 +200,7 @@
           end
 
   in
-    (add_edge_acyclic (node_id, dep) gr
+    ((add_edge_acyclic (node_id, dep) gr
         handle Graph.CYCLES _ => gr) handle Graph.UNDEF _ =>
          let
            val gr1 = add_edge (node_id, dep)
@@ -218,7 +218,8 @@
                 Pretty.string_of (Pretty.blk (0, separate Pretty.fbrk
                   (mk_gen_of_def gr2 "fun " descr') @ [Pretty.str ";"])) ^ "\n\n"
               else ""))) gr2
-         end
+         end,
+     module')
   end;
 
 
@@ -314,11 +315,12 @@
            let
              val (gr', ps) = foldl_map
                (invoke_tycodegen thy defs dep module false) (gr, Ts);
-             val gr'' = add_dt_defs thy defs dep module gr' descr
-           in SOME (gr'',
+             val (gr'', module') = add_dt_defs thy defs dep module gr' descr;
+             val (gr''', tyid) = mk_type_id module' s gr''
+           in SOME (gr''',
              Pretty.block ((if null Ts then [] else
                [mk_tuple ps, Pretty.str " "]) @
-               [Pretty.str (mk_qual_id module (get_type_id s gr''))]))
+               [Pretty.str (mk_qual_id module tyid)]))
            end)
   | datatype_tycodegen _ _ _ _ _ _ _ = NONE;