src/Pure/sign.ML
changeset 17405 e4dc583a2d79
parent 17343 098db1bc1e59
child 17412 e26cb20ef0cc
     1.1 --- a/src/Pure/sign.ML	Thu Sep 15 11:15:52 2005 +0200
     1.2 +++ b/src/Pure/sign.ML	Thu Sep 15 13:35:21 2005 +0200
     1.3 @@ -213,7 +213,8 @@
     1.4    val name = "Pure/sign";
     1.5    type T = sign;
     1.6    val copy = I;
     1.7 -  val extend = I;
     1.8 +  fun extend (Sign {syn, tsig, consts, ...}) =
     1.9 +    make_sign (NameSpace.default_naming, syn, tsig, consts);
    1.10  
    1.11    val empty = make_sign (NameSpace.default_naming, Syntax.pure_syn, Type.empty_tsig,
    1.12      (NameSpace.empty_table, Symtab.empty));