src/Pure/sign.ML
changeset 17405 e4dc583a2d79
parent 17343 098db1bc1e59
child 17412 e26cb20ef0cc
equal deleted inserted replaced
17404:d16c3a62c396 17405:e4dc583a2d79
   211 structure SignData = TheoryDataFun
   211 structure SignData = TheoryDataFun
   212 (struct
   212 (struct
   213   val name = "Pure/sign";
   213   val name = "Pure/sign";
   214   type T = sign;
   214   type T = sign;
   215   val copy = I;
   215   val copy = I;
   216   val extend = I;
   216   fun extend (Sign {syn, tsig, consts, ...}) =
       
   217     make_sign (NameSpace.default_naming, syn, tsig, consts);
   217 
   218 
   218   val empty = make_sign (NameSpace.default_naming, Syntax.pure_syn, Type.empty_tsig,
   219   val empty = make_sign (NameSpace.default_naming, Syntax.pure_syn, Type.empty_tsig,
   219     (NameSpace.empty_table, Symtab.empty));
   220     (NameSpace.empty_table, Symtab.empty));
   220 
   221 
   221   fun merge pp (sign1, sign2) =
   222   fun merge pp (sign1, sign2) =