changeset 8730 | d97ee7249698 |
parent 8725 | 0e48ee5b52db |
child 8802 | 2c37263eb903 |
--- 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 =