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));