# HG changeset patch
# User bulwahn
# Date 1307625261 -7200
# Node ID b017cfb10df4ffbde9f21bb84e076136094ec990
# Parent  e83695ea0e0a74535cc45a9795b4ed7c0d31cb07# Parent  2929f96d3ae7a34f264bf8a8dc554ddc6eaf1810
merged

diff -r 2929f96d3ae7 -r b017cfb10df4 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Thu Jun 09 14:24:34 2011 +0200
+++ b/src/Tools/Code/code_ml.ML	Thu Jun 09 15:14:21 2011 +0200
@@ -575,7 +575,8 @@
             (concat (
               str definer
               :: (str o deresolve) inst
-              :: print_dict_args vs
+              :: (if is_pseudo_fun inst then [str "()"]
+                  else print_dict_args vs)
               @ str "="
               @@ brackets [
                 enum_default "()" ";" "{" "}" (map print_super_instance super_instances