src/Pure/sign.ML
changeset 34259 2ba492b8b6e8
parent 34245 25bd3ed2ac9f
child 35129 ed24ba6f69aa
     1.1 --- a/src/Pure/sign.ML	Mon Jan 04 22:43:07 2010 +0100
     1.2 +++ b/src/Pure/sign.ML	Mon Jan 04 23:20:35 2010 +0100
     1.3 @@ -148,7 +148,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 = TheoryDataFun
     1.8 +structure SignData = Theory_Data_PP
     1.9  (
    1.10    type T = sign;
    1.11    fun extend (Sign {syn, tsig, consts, ...}) =