equal
deleted
inserted
replaced
63 (max (map (arg_nonempty o DatatypeAux.strip_dtyp) dts))) constrs) |
63 (max (map (arg_nonempty o DatatypeAux.strip_dtyp) dts))) constrs) |
64 in case xs of [] => NONE | x :: _ => SOME x end; |
64 in case xs of [] => NONE | x :: _ => SOME x end; |
65 |
65 |
66 fun add_dt_defs thy defs dep module gr (descr: DatatypeAux.descr) = |
66 fun add_dt_defs thy defs dep module gr (descr: DatatypeAux.descr) = |
67 let |
67 let |
68 val sg = sign_of thy; |
|
69 val tab = DatatypePackage.get_datatypes thy; |
68 val tab = DatatypePackage.get_datatypes thy; |
70 |
69 |
71 val descr' = List.filter (can (map DatatypeAux.dest_DtTFree o #2 o snd)) descr; |
70 val descr' = List.filter (can (map DatatypeAux.dest_DtTFree o #2 o snd)) descr; |
72 val rtnames = map (#1 o snd) (List.filter (fn (_, (_, _, cs)) => |
71 val rtnames = map (#1 o snd) (List.filter (fn (_, (_, _, cs)) => |
73 exists (exists DatatypeAux.is_rec_type o snd) cs) descr'); |
72 exists (exists DatatypeAux.is_rec_type o snd) cs) descr'); |