equal
deleted
inserted
replaced
40 |
40 |
41 (* datatype definition *) |
41 (* datatype definition *) |
42 |
42 |
43 fun add_dt_defs thy defs dep module (descr: Datatype.descr) sorts gr = |
43 fun add_dt_defs thy defs dep module (descr: Datatype.descr) sorts gr = |
44 let |
44 let |
45 val descr' = List.filter (can (map DatatypeAux.dest_DtTFree o #2 o snd)) descr; |
45 val descr' = filter (can (map DatatypeAux.dest_DtTFree o #2 o snd)) descr; |
46 val rtnames = map (#1 o snd) (List.filter (fn (_, (_, _, cs)) => |
46 val rtnames = map (#1 o snd) (filter (fn (_, (_, _, cs)) => |
47 exists (exists DatatypeAux.is_rec_type o snd) cs) descr'); |
47 exists (exists DatatypeAux.is_rec_type o snd) cs) descr'); |
48 |
48 |
49 val (_, (tname, _, _)) :: _ = descr'; |
49 val (_, (tname, _, _)) :: _ = descr'; |
50 val node_id = tname ^ " (type)"; |
50 val node_id = tname ^ " (type)"; |
51 val module' = if_library (thyname_of_type thy tname) module; |
51 val module' = if_library (thyname_of_type thy tname) module; |