src/Pure/sign.ML
changeset 72288 f8d28617ea08
parent 72283 4ed33ea8d957
equal deleted inserted replaced
72287:ce3f26b4e790 72288:f8d28617ea08
   134 fun make_sign (syn, tsig, consts) = Sign {syn = syn, tsig = tsig, consts = consts};
   134 fun make_sign (syn, tsig, consts) = Sign {syn = syn, tsig = tsig, consts = consts};
   135 
   135 
   136 structure Data = Theory_Data'
   136 structure Data = Theory_Data'
   137 (
   137 (
   138   type T = sign;
   138   type T = sign;
   139   fun extend (Sign {syn, tsig, consts, ...}) = make_sign (syn, tsig, consts);
   139   val extend = I;
   140 
       
   141   val empty = make_sign (Syntax.empty_syntax, Type.empty_tsig, Consts.empty);
   140   val empty = make_sign (Syntax.empty_syntax, Type.empty_tsig, Consts.empty);
   142 
       
   143   fun merge old_thys (sign1, sign2) =
   141   fun merge old_thys (sign1, sign2) =
   144     let
   142     let
   145       val Sign {syn = syn1, tsig = tsig1, consts = consts1} = sign1;
   143       val Sign {syn = syn1, tsig = tsig1, consts = consts1} = sign1;
   146       val Sign {syn = syn2, tsig = tsig2, consts = consts2} = sign2;
   144       val Sign {syn = syn2, tsig = tsig2, consts = consts2} = sign2;
   147 
   145