--- 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 *)