equal
deleted
inserted
replaced
721 |
721 |
722 fun reindex (DtType (s, dts)) = DtType (s, map reindex dts) |
722 fun reindex (DtType (s, dts)) = DtType (s, map reindex dts) |
723 | reindex (DtRec i) = DtRec (the (AList.lookup op = ty_idxs i)) |
723 | reindex (DtRec i) = DtRec (the (AList.lookup op = ty_idxs i)) |
724 | reindex dt = dt; |
724 | reindex dt = dt; |
725 |
725 |
726 fun strip_suffix i s = implode (List.take (explode s, size s - i)); |
726 fun strip_suffix i s = implode (List.take (raw_explode s, size s - i)); (* FIXME Symbol.explode (?) *) |
727 |
727 |
728 (** strips the "_Rep" in type names *) |
728 (** strips the "_Rep" in type names *) |
729 fun strip_nth_name i s = |
729 fun strip_nth_name i s = |
730 let val xs = Long_Name.explode s; |
730 let val xs = Long_Name.explode s; |
731 in Long_Name.implode (Library.nth_map (length xs - i) (strip_suffix 4) xs) end; |
731 in Long_Name.implode (Library.nth_map (length xs - i) (strip_suffix 4) xs) end; |