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;