Syntax.basic_syn;
authorwenzelm
Thu Jan 19 21:22:19 2006 +0100 (2006-01-19)
changeset 187141c310b042d69
parent 18713 cf777b9788b5
child 18715 f809deffdd8f
Syntax.basic_syn;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Thu Jan 19 21:22:18 2006 +0100
     1.2 +++ b/src/Pure/sign.ML	Thu Jan 19 21:22:19 2006 +0100
     1.3 @@ -211,7 +211,7 @@
     1.4      make_sign (NameSpace.default_naming, syn, tsig, consts);
     1.5  
     1.6    val empty =
     1.7 -    make_sign (NameSpace.default_naming, Syntax.pure_syn, Type.empty_tsig, Consts.empty);
     1.8 +    make_sign (NameSpace.default_naming, Syntax.basic_syn, Type.empty_tsig, Consts.empty);
     1.9  
    1.10    fun merge pp (sign1, sign2) =
    1.11      let