made SML/NJ happy;
authorwenzelm
Mon, 17 Apr 2000 14:20:41 +0200
changeset 8730 d97ee7249698
parent 8729 094dbd0fad0c
child 8731 085f0e32b9d6
made SML/NJ happy;
src/Pure/sign.ML
--- 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 =