# HG changeset patch
# User wenzelm
# Date 1369938387 -7200
# Node ID 4dced3d4155ce53b42cd8e67a80d81d78b843a81
# Parent  f4bf6b126cab282493bd8380772552b04e664c5f
standardized aliases;

diff -r f4bf6b126cab -r 4dced3d4155c src/HOL/Spec_Check/output_style.ML
--- a/src/HOL/Spec_Check/output_style.ML	Thu May 30 20:20:23 2013 +0200
+++ b/src/HOL/Spec_Check/output_style.ML	Thu May 30 20:26:27 2013 +0200
@@ -40,7 +40,7 @@
       ^ (padRight #" " countw (ratio (#count stats, length badobjs)))
 
     fun status (_, result, (stats, badobjs)) =
-      if Property.failure result then Output.writeln (update (stats, badobjs) false) else ()
+      if Property.failure result then writeln (update (stats, badobjs) false) else ()
 
     fun prtag count (tag, n) first =
       if String.isPrefix "__" tag then ("", first)
@@ -60,7 +60,7 @@
       let
         fun iter [] _ = ()
           | iter (e :: es) k =
-              (Output.writeln (padLeft #" " namew (if k > 0 then "" else "counter-examples")
+              (writeln (padLeft #" " namew (if k > 0 then "" else "counter-examples")
                 ^ padRight #" " resultw (if k > 0 then "" else ":") ^ e);
               iter es (k + 1))
       in
@@ -68,8 +68,8 @@
       end
 
     fun finish (stats, badobjs) =
-      if null badobjs then Output.writeln (update (stats, badobjs) true ^ prtags stats)
-      else (Output.writeln (update (stats, badobjs) true); err badobjs)
+      if null badobjs then writeln (update (stats, badobjs) true ^ prtags stats)
+      else (writeln (update (stats, badobjs) true); err badobjs)
   in
     {status=status, finish=finish}
   end
@@ -92,19 +92,19 @@
 fun new ctxt tag =
   let
     val gen_target = Config.get_generic ctxt Spec_Check.gen_target
-    val _ = Output.writeln ("[testing " ^ tag ^ "... ") (* TODO: Output without line break *)
+    val _ = writeln ("[testing " ^ tag ^ "... ") (* TODO: Output without line break *)
     fun finish ({count, ...}, badobjs) = case (count, badobjs) of
-        (0, []) => Output.writeln ("no valid cases generated]")
-      | (n, []) => Output.writeln (
+        (0, []) => writeln ("no valid cases generated]")
+      | (n, []) => writeln (
             if n >= gen_target then "ok]"
             else "ok on " ^ string_of_int n ^ "; " ^ string_of_int gen_target ^ " required]")
       | (_, es) =>
         let
           val wd = size (string_of_int (length es))
           fun each (NONE, _) = ()
-            | each (SOME e, i) = Output.writeln (tag ^ ":" ^ pad wd i ^ ".0 Error: " ^ e)
+            | each (SOME e, i) = writeln (tag ^ ":" ^ pad wd i ^ ".0 Error: " ^ e)
          in
-           (Output.writeln "FAILED]"; map each (es ~~ (1 upto (length es))); ())
+           (writeln "FAILED]"; map each (es ~~ (1 upto (length es))); ())
          end
   in
     {status = K (), finish = finish}