src/Pure/sign.ML
changeset 18714 1c310b042d69
parent 18678 dd0c569fa43d
child 18857 c4b4fbd74ffb
--- 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