src/Pure/sign.ML
changeset 4007 1d6aed7ff375
parent 3995 88fc1015d241
child 4017 63878e2587a7
     1.1 --- a/src/Pure/sign.ML	Mon Oct 27 10:34:17 1997 +0100
     1.2 +++ b/src/Pure/sign.ML	Mon Oct 27 10:46:36 1997 +0100
     1.3 @@ -754,10 +754,10 @@
     1.4        (path, add_names spaces constK (map fst decls)), data)
     1.5    end;
     1.6  
     1.7 -val ext_consts_i = ext_cnsts no_read false ("", true);
     1.8 -val ext_consts = ext_cnsts read_const false ("", true);
     1.9 -val ext_syntax_i = ext_cnsts no_read true ("", true);
    1.10 -val ext_syntax = ext_cnsts read_const true ("", true);
    1.11 +fun ext_consts_i sg = ext_cnsts no_read false ("", true) sg;
    1.12 +fun ext_consts sg = ext_cnsts read_const false ("", true) sg;
    1.13 +fun ext_syntax_i sg = ext_cnsts no_read true ("", true) sg;
    1.14 +fun ext_syntax sg = ext_cnsts read_const true ("", true) sg;
    1.15  fun ext_modesyntax_i sg (prmode, consts) = ext_cnsts no_read true prmode sg consts;
    1.16  fun ext_modesyntax sg (prmode, consts) = ext_cnsts read_const true prmode sg consts;
    1.17