merged
authorbulwahn
Thu, 09 Jun 2011 15:14:21 +0200
changeset 43344 b017cfb10df4
parent 43343 e83695ea0e0a (diff)
parent 43342 2929f96d3ae7 (current diff)
child 43345 165188299a25
merged
--- 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