src/Pure/sign.ML
changeset 18714 1c310b042d69
parent 18678 dd0c569fa43d
child 18857 c4b4fbd74ffb
equal deleted inserted replaced
18713:cf777b9788b5 18714:1c310b042d69
   209   val copy = I;
   209   val copy = I;
   210   fun extend (Sign {syn, tsig, consts, ...}) =
   210   fun extend (Sign {syn, tsig, consts, ...}) =
   211     make_sign (NameSpace.default_naming, syn, tsig, consts);
   211     make_sign (NameSpace.default_naming, syn, tsig, consts);
   212 
   212 
   213   val empty =
   213   val empty =
   214     make_sign (NameSpace.default_naming, Syntax.pure_syn, Type.empty_tsig, Consts.empty);
   214     make_sign (NameSpace.default_naming, Syntax.basic_syn, Type.empty_tsig, Consts.empty);
   215 
   215 
   216   fun merge pp (sign1, sign2) =
   216   fun merge pp (sign1, sign2) =
   217     let
   217     let
   218       val Sign {naming = _, syn = syn1, tsig = tsig1, consts = consts1} = sign1;
   218       val Sign {naming = _, syn = syn1, tsig = tsig1, consts = consts1} = sign1;
   219       val Sign {naming = _, syn = syn2, tsig = tsig2, consts = consts2} = sign2;
   219       val Sign {naming = _, syn = syn2, tsig = tsig2, consts = consts2} = sign2;