| changeset 34259 | 2ba492b8b6e8 |
| parent 34245 | 25bd3ed2ac9f |
| child 35845 | e5980f0ad025 |
--- a/src/Pure/theory.ML Mon Jan 04 22:43:07 2010 +0100 +++ b/src/Pure/theory.ML Mon Jan 04 23:20:35 2010 +0100 @@ -86,7 +86,7 @@ fun make_thy (axioms, defs, wrappers) = Thy {axioms = axioms, defs = defs, wrappers = wrappers}; -structure ThyData = TheoryDataFun +structure ThyData = Theory_Data_PP ( type T = thy; val empty_axioms = Name_Space.empty_table "axiom" : term Name_Space.table;