# HG changeset patch
# User wenzelm
# Date 1369944906 -7200
# Node ID 3de2666b089da60944191089acdc8ca3201a12f5
# Parent  e7c47fe56fbdb9bff8a9550fa79d48816cfa6664
tuned;

diff -r e7c47fe56fbd -r 3de2666b089d src/HOL/Spec_Check/output_style.ML
--- a/src/HOL/Spec_Check/output_style.ML	Thu May 30 22:11:29 2013 +0200
+++ b/src/HOL/Spec_Check/output_style.ML	Thu May 30 22:15:06 2013 +0200
@@ -40,7 +40,8 @@
 
         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)"
+          | ratio (count, n) =
+              "(" ^ string_of_int (count - n) ^ "/" ^ string_of_int count ^  " passed)"
 
         fun update (stats, badobjs) donep =
           "\r" ^ StringCvt.padRight #"." namew tag ^ "." ^