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