author | wenzelm |
Mon, 17 Apr 2000 14:20:41 +0200 | |
changeset 8730 | d97ee7249698 |
parent 8729 | 094dbd0fad0c |
child 8731 | 085f0e32b9d6 |
src/Pure/sign.ML | file | annotate | diff | comparison | revisions |
--- a/src/Pure/sign.ML Mon Apr 17 14:12:33 2000 +0200 +++ b/src/Pure/sign.ML Mon Apr 17 14:20:41 2000 +0200 @@ -422,8 +422,8 @@ (*add / hide names*) fun change_space f spaces kind x = overwrite (spaces, (kind, f (space_of spaces kind, x))); -val add_names = change_space NameSpace.extend; -val hide_names = change_space NameSpace.hide; +fun add_names x = change_space NameSpace.extend x; +fun hide_names x = change_space NameSpace.hide x; (*make full names*) fun full path name =