--- a/src/Pure/ML-Systems/proper_int.ML Fri May 31 09:30:32 2013 +0200
+++ b/src/Pure/ML-Systems/proper_int.ML Fri May 31 11:56:48 2013 +0200
@@ -85,6 +85,15 @@
end;
+(* CharVector *)
+
+structure CharVector =
+struct
+ open CharVector;
+ fun tabulate (a, b) = CharVector.tabulate (dest_int a, b o mk_int);
+end;
+
+
(* Word8VectorSlice *)
structure Word8VectorSlice =
@@ -157,6 +166,8 @@
| GEN (SOME b) => StringCvt.GEN (SOME (dest_int b))
| SCI NONE => StringCvt.SCI NONE
| SCI (SOME b) => StringCvt.SCI (SOME (dest_int b)));
+ fun padRight a b c = StringCvt.padRight a (dest_int b) c;
+ fun padLeft a b c = StringCvt.padLeft a (dest_int b) c;
end;