# HG changeset patch
# User wenzelm
# Date 955974430 -7200
# Node ID 085f0e32b9d61f65f6743acd28b5e431f7b4aade
# Parent  d97ee72496984390909eef7c83f5c36adaa8259b
made SML/NJ happy;

diff -r d97ee7249698 -r 085f0e32b9d6 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Mon Apr 17 14:20:41 2000 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Mon Apr 17 14:27:10 2000 +0200
@@ -203,8 +203,8 @@
   if kind mem_string [Sign.classK, Sign.typeK, Sign.constK] then f (kind, names) thy
   else error ("Bad name space specification: " ^ quote kind);
 
-val hide_space = gen_hide Theory.hide_space;
-val hide_space_i = gen_hide Theory.hide_space_i;
+fun hide_space x = gen_hide Theory.hide_space x;
+fun hide_space_i x = gen_hide Theory.hide_space_i x;
 
 
 (* signature and syntax *)