# HG changeset patch
# User wenzelm
# Date 1369943268 -7200
# Node ID 24f59223430da71a7a45ef0ded2694bf76713111
# Parent  85f732610740c44023f4577312ea4db050b16cb5
do not open ML structures;

diff -r 85f732610740 -r 24f59223430d src/HOL/Spec_Check/base_generator.ML
--- a/src/HOL/Spec_Check/base_generator.ML	Thu May 30 21:37:00 2013 +0200
+++ b/src/HOL/Spec_Check/base_generator.ML	Thu May 30 21:47:48 2013 +0200
@@ -91,15 +91,15 @@
 
 fun lift obj r = (obj, r)
 
-local open Vector (* Isabelle does not use vectors? *)
-      fun explode ((freq, gen), acc) =
-          List.tabulate (freq, fn _ => gen) @ acc
-in fun choose v r =
-       let val (i, r) = range(0, length v - 1) r
-        in sub (v, i) r
-       end
-   fun choose' v = choose (fromList (foldr explode nil v))
-   fun select v = choose (map lift v)
+local (* Isabelle does not use vectors? *)
+  fun explode ((freq, gen), acc) =
+    List.tabulate (freq, fn _ => gen) @ acc
+in
+  fun choose v r =
+    let val (i, r) = range(0, Vector.length v - 1) r
+    in Vector.sub (v, i) r end
+  fun choose' v = choose (Vector.fromList (Vector.foldr explode nil v))
+  fun select v = choose (Vector.map lift v)
 end
 
 fun chooseL l = choose (Vector.fromList l)
diff -r 85f732610740 -r 24f59223430d src/HOL/Spec_Check/generator.ML
--- a/src/HOL/Spec_Check/generator.ML	Thu May 30 21:37:00 2013 +0200
+++ b/src/HOL/Spec_Check/generator.ML	Thu May 30 21:47:48 2013 +0200
@@ -57,7 +57,6 @@
 
 (* text *)
 
-open Text
 type char = Char.char
 type string = String.string
 type substring = Substring.substring
@@ -74,9 +73,10 @@
 val string = vector CharVector.tabulate
 
 fun substring gen r =
-  let val (s, r') = gen r
-      val (i, r'') = range (0, String.size s) r'
-      val (j, r''') = range (0, String.size s - i) r''
+  let
+    val (s, r') = gen r
+    val (i, r'') = range (0, String.size s) r'
+    val (j, r''') = range (0, String.size s - i) r''
   in
     (Substring.substring (s, i, j), r''')
   end
diff -r 85f732610740 -r 24f59223430d src/HOL/Spec_Check/output_style.ML
--- a/src/HOL/Spec_Check/output_style.ML	Thu May 30 21:37:00 2013 +0200
+++ b/src/HOL/Spec_Check/output_style.ML	Thu May 30 21:47:48 2013 +0200
@@ -17,8 +17,6 @@
 
 local
 
-open StringCvt
-
 fun new ctxt tag =
   let
     val target = Config.get ctxt Spec_Check.gen_target
@@ -45,8 +43,9 @@
       | ratio (count, n) = "(" ^ string_of_int (count - n) ^ "/" ^ string_of_int count ^  " passed)"
 
     fun update (stats, badobjs) donep =
-      "\r" ^ padRight #"." namew tag ^ "." ^ padRight #" " resultw (result (stats, badobjs) donep)
-      ^ padRight #" " countw (ratio (#count stats, length badobjs))
+      "\r" ^ StringCvt.padRight #"." namew tag ^ "." ^
+      StringCvt.padRight #" " resultw (result (stats, badobjs) donep) ^
+      StringCvt.padRight #" " countw (ratio (#count stats, length badobjs))
 
     fun status (_, result, (stats, badobjs)) =
       if Property.failure result then writeln (update (stats, badobjs) false) else ()
@@ -57,8 +56,8 @@
          let
            val ratio = round ((real n / real count) * 100.0)
          in
-           (((if first then "" else padRight #" " allw "\n") ^
-             padLeft #" " 3 (string_of_int ratio) ^ "% " ^ tag),
+           (((if first then "" else StringCvt.padRight #" " allw "\n") ^
+             StringCvt.padLeft #" " 3 (string_of_int ratio) ^ "% " ^ tag),
            false)
          end
 
@@ -69,8 +68,8 @@
       let
         fun iter [] _ = ()
           | iter (e :: es) k =
-              (writeln (padLeft #" " namew (if k > 0 then "" else "counter-examples")
-                ^ padRight #" " resultw (if k > 0 then "" else ":") ^ e);
+              (writeln (StringCvt.padLeft #" " namew (if k > 0 then "" else "counter-examples") ^
+                StringCvt.padRight #" " resultw (if k > 0 then "" else ":") ^ e);
               iter es (k + 1))
       in
         iter (maybe_sort (take limit (map_filter I badobjs))) 0
diff -r 85f732610740 -r 24f59223430d src/HOL/Spec_Check/spec_check.ML
--- a/src/HOL/Spec_Check/spec_check.ML	Thu May 30 21:37:00 2013 +0200
+++ b/src/HOL/Spec_Check/spec_check.ML	Thu May 30 21:47:48 2013 +0200
@@ -41,8 +41,6 @@
 val column_width = Attrib.setup_config_int @{binding spec_check_column_width} (K 22)
 val style = Attrib.setup_config_string @{binding spec_check_style} (K "Perl")
 
-open Property
-
 type ('a, 'b) reader = 'b -> ('a * 'b) option
 type 'a rep = ('a -> string) option