tuned;
authorwenzelm
Mon Mar 15 21:59:28 2010 +0100 (2010-03-15)
changeset 35801952308389b8b
parent 35800 76b2a53a199d
child 35804 4046a6111838
tuned;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Mon Mar 15 21:57:35 2010 +0100
     1.2 +++ b/src/Pure/sign.ML	Mon Mar 15 21:59:28 2010 +0100
     1.3 @@ -142,7 +142,7 @@
     1.4  fun make_sign (naming, syn, tsig, consts) =
     1.5    Sign {naming = naming, syn = syn, tsig = tsig, consts = consts};
     1.6  
     1.7 -structure SignData = Theory_Data_PP
     1.8 +structure Data = Theory_Data_PP
     1.9  (
    1.10    type T = sign;
    1.11    fun extend (Sign {syn, tsig, consts, ...}) =
    1.12 @@ -163,9 +163,9 @@
    1.13      in make_sign (naming, syn, tsig, consts) end;
    1.14  );
    1.15  
    1.16 -fun rep_sg thy = SignData.get thy |> (fn Sign args => args);
    1.17 +fun rep_sg thy = Data.get thy |> (fn Sign args => args);
    1.18  
    1.19 -fun map_sign f = SignData.map (fn Sign {naming, syn, tsig, consts} =>
    1.20 +fun map_sign f = Data.map (fn Sign {naming, syn, tsig, consts} =>
    1.21    make_sign (f (naming, syn, tsig, consts)));
    1.22  
    1.23  fun map_naming f = map_sign (fn (naming, syn, tsig, consts) => (f naming, syn, tsig, consts));