# HG changeset patch
# User wenzelm
# Date 955974041 -7200
# Node ID d97ee72496984390909eef7c83f5c36adaa8259b
# Parent  094dbd0fad0c3035fd11c1f31094e62b3c56e0cf
made SML/NJ happy;

diff -r 094dbd0fad0c -r d97ee7249698 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 =