# HG changeset patch
# User webertj
# Date 1147083837 -7200
# Node ID 846f0d5bfc832ba40ca4d83931ac6ec287ebfe52
# Parent  eb063e7932d7ec3ac770ffc97ac8f2e42d23f88f
string_of_option tuned

diff -r eb063e7932d7 -r 846f0d5bfc83 src/Pure/library.ML
--- a/src/Pure/library.ML	Sun May 07 00:47:07 2006 +0200
+++ b/src/Pure/library.ML	Mon May 08 12:23:57 2006 +0200
@@ -374,7 +374,7 @@
   | merge_opt eq (SOME x, SOME y) = if eq (x, y) then SOME y else raise Option;
 
 fun string_of_option f NONE     = "NONE"
-  | string_of_option f (SOME x) = "SOME " ^ f x;
+  | string_of_option f (SOME x) = "SOME (" ^ f x ^ ")";
 
 
 (* exceptions *)