changeset 43343 | e83695ea0e0a |
parent 42599 | 1a82b0400b2a |
child 43345 | 165188299a25 |
--- a/src/Tools/Code/code_ml.ML Thu Jun 09 11:57:39 2011 +0200 +++ b/src/Tools/Code/code_ml.ML Thu Jun 09 14:16:12 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