author | wenzelm |
Thu, 19 Jan 2006 21:22:19 +0100 | |
changeset 18714 | 1c310b042d69 |
parent 18713 | cf777b9788b5 |
child 18715 | f809deffdd8f |
src/Pure/sign.ML | file | annotate | diff | comparison | revisions |
--- a/src/Pure/sign.ML Thu Jan 19 21:22:18 2006 +0100 +++ b/src/Pure/sign.ML Thu Jan 19 21:22:19 2006 +0100 @@ -211,7 +211,7 @@ make_sign (NameSpace.default_naming, syn, tsig, consts); val empty = - make_sign (NameSpace.default_naming, Syntax.pure_syn, Type.empty_tsig, Consts.empty); + make_sign (NameSpace.default_naming, Syntax.basic_syn, Type.empty_tsig, Consts.empty); fun merge pp (sign1, sign2) = let