equal
deleted
inserted
replaced
44 val rtnames = map (#1 o snd) (List.filter (fn (_, (_, _, cs)) => |
44 val rtnames = map (#1 o snd) (List.filter (fn (_, (_, _, cs)) => |
45 exists (exists DatatypeAux.is_rec_type o snd) cs) descr'); |
45 exists (exists DatatypeAux.is_rec_type o snd) cs) descr'); |
46 |
46 |
47 val (_, (tname, _, _)) :: _ = descr'; |
47 val (_, (tname, _, _)) :: _ = descr'; |
48 val node_id = tname ^ " (type)"; |
48 val node_id = tname ^ " (type)"; |
49 val module' = if_library (thyname_of_type tname thy) module; |
49 val module' = if_library (thyname_of_type thy tname) module; |
50 |
50 |
51 fun mk_dtdef gr prfx [] = (gr, []) |
51 fun mk_dtdef gr prfx [] = (gr, []) |
52 | mk_dtdef gr prfx ((_, (tname, dts, cs))::xs) = |
52 | mk_dtdef gr prfx ((_, (tname, dts, cs))::xs) = |
53 let |
53 let |
54 val tvs = map DatatypeAux.dest_DtTFree dts; |
54 val tvs = map DatatypeAux.dest_DtTFree dts; |