# HG changeset patch
# User wenzelm
# Date 877945596 -3600
# Node ID 1d6aed7ff375fdf1aaa1f8c4cfc905b4a61c2067
# Parent  84a5efc95dcfe0be99e5a7ce84f7278d38aa447a
made SML/NJ happy;

diff -r 84a5efc95dcf -r 1d6aed7ff375 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Mon Oct 27 10:34:17 1997 +0100
+++ b/src/Pure/sign.ML	Mon Oct 27 10:46:36 1997 +0100
@@ -754,10 +754,10 @@
       (path, add_names spaces constK (map fst decls)), data)
   end;
 
-val ext_consts_i = ext_cnsts no_read false ("", true);
-val ext_consts = ext_cnsts read_const false ("", true);
-val ext_syntax_i = ext_cnsts no_read true ("", true);
-val ext_syntax = ext_cnsts read_const true ("", true);
+fun ext_consts_i sg = ext_cnsts no_read false ("", true) sg;
+fun ext_consts sg = ext_cnsts read_const false ("", true) sg;
+fun ext_syntax_i sg = ext_cnsts no_read true ("", true) sg;
+fun ext_syntax sg = ext_cnsts read_const true ("", true) sg;
 fun ext_modesyntax_i sg (prmode, consts) = ext_cnsts no_read true prmode sg consts;
 fun ext_modesyntax sg (prmode, consts) = ext_cnsts read_const true prmode sg consts;