Fixed bug concerning the generation of identifiers for
authorberghofe
Fri Sep 22 14:36:23 2006 +0200 (2006-09-22)
changeset 206810e4df994ad34
parent 20680 fd92d9310128
child 20682 cecff1f51431
Fixed bug concerning the generation of identifiers for
datatypes, which caused the code generator to fail for
mutually recursive datatypes.
src/HOL/Tools/datatype_codegen.ML
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Fri Sep 22 14:32:46 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Fri Sep 22 14:36:23 2006 +0200
     1.3 @@ -200,7 +200,7 @@
     1.4            end
     1.5  
     1.6    in
     1.7 -    (add_edge_acyclic (node_id, dep) gr
     1.8 +    ((add_edge_acyclic (node_id, dep) gr
     1.9          handle Graph.CYCLES _ => gr) handle Graph.UNDEF _ =>
    1.10           let
    1.11             val gr1 = add_edge (node_id, dep)
    1.12 @@ -218,7 +218,8 @@
    1.13                  Pretty.string_of (Pretty.blk (0, separate Pretty.fbrk
    1.14                    (mk_gen_of_def gr2 "fun " descr') @ [Pretty.str ";"])) ^ "\n\n"
    1.15                else ""))) gr2
    1.16 -         end
    1.17 +         end,
    1.18 +     module')
    1.19    end;
    1.20  
    1.21  
    1.22 @@ -314,11 +315,12 @@
    1.23             let
    1.24               val (gr', ps) = foldl_map
    1.25                 (invoke_tycodegen thy defs dep module false) (gr, Ts);
    1.26 -             val gr'' = add_dt_defs thy defs dep module gr' descr
    1.27 -           in SOME (gr'',
    1.28 +             val (gr'', module') = add_dt_defs thy defs dep module gr' descr;
    1.29 +             val (gr''', tyid) = mk_type_id module' s gr''
    1.30 +           in SOME (gr''',
    1.31               Pretty.block ((if null Ts then [] else
    1.32                 [mk_tuple ps, Pretty.str " "]) @
    1.33 -               [Pretty.str (mk_qual_id module (get_type_id s gr''))]))
    1.34 +               [Pretty.str (mk_qual_id module tyid)]))
    1.35             end)
    1.36    | datatype_tycodegen _ _ _ _ _ _ _ = NONE;
    1.37