minor tuning -- more linebreaks;

--- a/src/HOL/Spec_Check/output_style.ML	Thu May 30 20:27:33 2013 +0200
+++ b/src/HOL/Spec_Check/output_style.ML	Thu May 30 20:38:50 2013 +0200
@@ -28,16 +28,18 @@
 
     fun result ({count=0,...}, _) _ = "dubious"
       | result (_ : Property.stats, badobjs) false = if null badobjs then "ok" else "FAILED"
-      | 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"
+      | 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"
 
     fun ratio (0, _) = "(0/0 passed)"
       | ratio (count, 0) = "(" ^ string_of_int count ^ " passed)"
       | 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" ^ padRight #"." namew tag ^ "." ^ padRight #" " resultw (result (stats, badobjs) donep)
+      ^ padRight #" " countw (ratio (#count stats, length badobjs))
 
     fun status (_, result, (stats, badobjs)) =
       if Property.failure result then writeln (update (stats, badobjs) false) else ()
@@ -93,7 +95,8 @@
   let
     val gen_target = Config.get_generic ctxt Spec_Check.gen_target
     val _ = writeln ("[testing " ^ tag ^ "... ")
-    fun finish ({count, ...}, badobjs) = case (count, badobjs) of
+    fun finish ({count, ...}, badobjs) =
+      (case (count, badobjs) of
         (0, []) => writeln ("no valid cases generated]")
       | (n, []) => writeln (
             if n >= gen_target then "ok]"
@@ -105,7 +108,7 @@
             | each (SOME e, i) = writeln (tag ^ ":" ^ pad wd i ^ ".0 Error: " ^ e)
          in
            (writeln "FAILED]"; map each (es ~~ (1 upto (length es))); ())
-         end
+         end)
   in
     {status = K (), finish = finish}
   end

--- a/src/HOL/Spec_Check/property.ML	Thu May 30 20:27:33 2013 +0200
+++ b/src/HOL/Spec_Check/property.ML	Thu May 30 20:38:50 2013 +0200
@@ -56,9 +56,13 @@
 
 fun classify' f =
   wrap (fn (x, result, {tags, count}) =>
-    { tags = if is_some result then
-        case f x of NONE => tags | SOME tag => AList.map_default (op =) (tag, 0) (fn c => c + 1) tags
-      else tags, count = count })
+    { tags =
+        if is_some result then
+          (case f x of
+            NONE => tags
+          | SOME tag => AList.map_default (op =) (tag, 0) (fn c => c + 1) tags)
+        else tags,
+     count = count })
 
 fun classify p tag = classify' (fn x => if p x then SOME tag else NONE)
 

--- a/src/HOL/Spec_Check/spec_check.ML	Thu May 30 20:27:33 2013 +0200
+++ b/src/HOL/Spec_Check/spec_check.ML	Thu May 30 20:38:50 2013 +0200
@@ -7,7 +7,6 @@
 
 signature SPEC_CHECK =
 sig
-
   val gen_target : int Config.T
   val gen_max : int Config.T
   val examples : int Config.T
@@ -17,11 +16,13 @@
   val style : string Config.T
 
   type output_style = Context.generic -> string ->
-    {status : string option * Property.result * (Property.stats  * string option list) -> unit, finish: Property.stats * string option list -> unit}
+    {status : string option * Property.result * (Property.stats  * string option list) -> unit,
+     finish: Property.stats * string option list -> unit}
 
   val register_style : (string * output_style) -> theory -> theory
 
-  val checkGen : Context.generic -> 'a Generator.gen * ('a -> string) option -> string * 'a Property.prop -> unit
+  val checkGen : Context.generic ->
+    'a Generator.gen * ('a -> string) option -> string * 'a Property.prop -> unit
 
   val check_property : Proof.context -> string -> unit
 end;
@@ -46,7 +47,8 @@
 type 'a rep = ('a -> string) option
 
 type output_style = Context.generic -> string ->
-  {status: string option * Property.result * (Property.stats * string option list) -> unit, finish: Property.stats * string option list -> unit}
+  {status: string option * Property.result * (Property.stats * string option list) -> unit,
+   finish: Property.stats * string option list -> unit}
 
 fun limit ctxt gen = Generator.limit (Config.get_generic ctxt gen_max) gen
 
@@ -112,13 +114,14 @@
 fun checks ctxt = cpsCheck ctxt Property.stats
 
 fun checkGen ctxt (gen, show) (tag, prop) =
-    check' ctxt {count=0, tags=[("__GEN", 0)]} (limit ctxt gen, show) (tag, prop) Generator.stream
+  check' ctxt {count=0, tags=[("__GEN", 0)]} (limit ctxt gen, show) (tag, prop) Generator.stream
 
 fun checkGenShrink ctxt shrink (gen, show) (tag, prop) =
-    cpsCheck ctxt {count=0, tags=[("__GEN", 0)]} shrink
-           (limit ctxt gen, show) (tag, prop) Generator.stream
+  cpsCheck ctxt {count=0, tags=[("__GEN", 0)]} shrink
+    (limit ctxt gen, show) (tag, prop) Generator.stream
 
-fun checkOne ctxt show (tag, prop) obj = check ctxt (List.getItem, show) (tag, prop) [obj]
+fun checkOne ctxt show (tag, prop) obj =
+  check ctxt (List.getItem, show) (tag, prop) [obj]
 
 (*calls the compiler and passes resulting type string to the parser*)
 fun determine_type context s =
@@ -140,7 +143,8 @@
 (*calls the compiler and runs the test*)
 fun run_test context s =
   let
-    val _ = Context.proof_map
+    val _ =
+      Context.proof_map
         (ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code")
         true s)) context
   in () end;
@@ -152,7 +156,8 @@
     fun space c = c = #" "
     val (head, code) = Substring.splitl (not o dot) (Substring.full s)
   in (String.tokens space (Substring.string head),
-    Substring.string (Substring.dropl dot code)) end;
+    Substring.string (Substring.dropl dot code))
+  end;
 
 (*create the function from the input*)
 fun make_fun s =