Syntax.basic_syn;
authorwenzelm
Thu, 19 Jan 2006 21:22:19 +0100
changeset 18714 1c310b042d69
parent 18713 cf777b9788b5
child 18715 f809deffdd8f
Syntax.basic_syn;
src/Pure/sign.ML
--- 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