974 | vs => error ("Extra type variables on rhs: " ^ commas vs)) |
974 | vs => error ("Extra type variables on rhs: " ^ commas vs)) |
975 in (constrs @ [((if flat_names then Sign.full_name sign else |
975 in (constrs @ [((if flat_names then Sign.full_name sign else |
976 Sign.full_name_path sign tname) (Syntax.const_name cname mx'), |
976 Sign.full_name_path sign tname) (Syntax.const_name cname mx'), |
977 map (dtyp_of_typ new_dts) cargs')], |
977 map (dtyp_of_typ new_dts) cargs')], |
978 constr_syntax' @ [(cname, mx')], sorts'') |
978 constr_syntax' @ [(cname, mx')], sorts'') |
979 end handle ERROR => |
979 end handle ERROR msg => |
980 error ("The error above occured in constructor " ^ cname ^ |
980 cat_error msg ("The error above occured in constructor " ^ cname ^ |
981 " of datatype " ^ tname); |
981 " of datatype " ^ tname); |
982 |
982 |
983 val (constrs', constr_syntax', sorts') = |
983 val (constrs', constr_syntax', sorts') = |
984 Library.foldl prep_constr (([], [], sorts), constrs) |
984 Library.foldl prep_constr (([], [], sorts), constrs) |
985 |
985 |