# HG changeset patch
# User wenzelm
# Date 1369994208 -7200
# Node ID 2bbeab01c0eae161276f5c9f5727c0bb6b91be12
# Parent  329c4143815462d06322e86040afde0a24997cf5
make SML/NJ partially happy;

diff -r 329c41438154 -r 2bbeab01c0ea src/HOL/ROOT
--- a/src/HOL/ROOT	Fri May 31 09:30:32 2013 +0200
+++ b/src/HOL/ROOT	Fri May 31 11:56:48 2013 +0200
@@ -742,6 +742,8 @@
 
 session "HOL-Spec_Check" in Spec_Check = HOL +
   theories
+    Spec_Check
+  theories [condition = ISABELLE_POLYML]
     Examples
 
 session "HOL-Statespace" in Statespace = HOL +
diff -r 329c41438154 -r 2bbeab01c0ea src/HOL/Spec_Check/output_style.ML
--- a/src/HOL/Spec_Check/output_style.ML	Fri May 31 09:30:32 2013 +0200
+++ b/src/HOL/Spec_Check/output_style.ML	Fri May 31 11:56:48 2013 +0200
@@ -31,9 +31,9 @@
 
         val maybe_sort = if sort_examples then sort (int_ord o pairself size) else I
 
-        fun result ({count=0,...}, _) _ = "dubious"
+        fun result ({count = 0, ...}, _) _ = "dubious"
           | result (_ : Property.stats, badobjs) false = if null badobjs then "ok" else "FAILED"
-          | result ({count,tags,...}, badobjs) true =
+          | result ({count, tags}, badobjs) true =
               if not (null badobjs) then "FAILED"
               else if AList.defined (op =) tags "__GEN" andalso count < target then "dubious"
               else "ok"
@@ -62,7 +62,7 @@
                false)
              end
 
-        fun prtags ({count, tags, ...} : Property.stats) =
+        fun prtags ({count, tags} : Property.stats) =
           if show_stats then cat_lines (fst (fold_map (prtag count) tags true)) else ""
 
         fun err badobjs =
@@ -93,7 +93,7 @@
         fun pad wd = StringCvt.padLeft #"0" wd o Int.toString
         val gen_target = Config.get ctxt Spec_Check.gen_target
         val _ = writeln ("[testing " ^ tag ^ "... ")
-        fun finish ({count, ...}, badobjs) =
+        fun finish ({count, ...} : Property.stats, badobjs) =
           (case (count, badobjs) of
             (0, []) => warning ("no valid cases generated]")
           | (n, []) => writeln (
diff -r 329c41438154 -r 2bbeab01c0ea src/Pure/ML-Systems/proper_int.ML
--- 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;