# HG changeset patch
# User wenzelm
# Date 1137702139 -3600
# Node ID 1c310b042d6950b2b255e89efd8d292136fa9207
# Parent  cf777b9788b55b0b5cefac8ce3eb462de259b80a
Syntax.basic_syn;

diff -r cf777b9788b5 -r 1c310b042d69 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