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