src/Pure/ML-Systems/proper_int.ML

       NONE => NONE
     | SOME (c, d) => SOME (mk_int c, d));
 end;
 
 
+(* CharVector *)
+
+structure CharVector =
+struct
+  open CharVector;
+  fun tabulate (a, b) = CharVector.tabulate (dest_int a, b o mk_int);
+end;
+
+
 (* Word8VectorSlice *)
 
 structure Word8VectorSlice =
 struct
   open Word8VectorSlice;

     | FIX (SOME b) => StringCvt.FIX (SOME (dest_int b))
     | GEN NONE => StringCvt.GEN NONE
     | 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;
 
 
 (* Word *)