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