# 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 ^ "." ^