# HG changeset patch
# User wenzelm
# Date 1126784121 -7200
# Node ID e4dc583a2d797ecc9c78234b4897dd7ec80c7d4e
# Parent  d16c3a62c396f5dc58214f48be9edaadbdd22074
extend: NameSpace.default_naming;

diff -r d16c3a62c396 -r e4dc583a2d79 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Thu Sep 15 11:15:52 2005 +0200
+++ b/src/Pure/sign.ML	Thu Sep 15 13:35:21 2005 +0200
@@ -213,7 +213,8 @@
   val name = "Pure/sign";
   type T = sign;
   val copy = I;
-  val extend = I;
+  fun extend (Sign {syn, tsig, consts, ...}) =
+    make_sign (NameSpace.default_naming, syn, tsig, consts);
 
   val empty = make_sign (NameSpace.default_naming, Syntax.pure_syn, Type.empty_tsig,
     (NameSpace.empty_table, Symtab.empty));