src/Pure/theory.ML
changeset 42016 3b6826b3ed37
parent 39134 917b4b6ba3d2
child 42360 da8817d01e7c
--- a/src/Pure/theory.ML	Sun Mar 20 22:26:43 2011 +0100
+++ b/src/Pure/theory.ML	Sun Mar 20 22:47:08 2011 +0100
@@ -84,7 +84,7 @@
 
 fun make_thy (axioms, defs, wrappers) = Thy {axioms = axioms, defs = defs, wrappers = wrappers};
 
-structure ThyData = Theory_Data_PP
+structure Thy = Theory_Data_PP
 (
   type T = thy;
   val empty_axioms = Name_Space.empty_table "axiom" : term Name_Space.table;
@@ -104,9 +104,9 @@
     in make_thy (axioms', defs', (bgs', ens')) end;
 );
 
-fun rep_theory thy = ThyData.get thy |> (fn Thy args => args);
+fun rep_theory thy = Thy.get thy |> (fn Thy args => args);
 
-fun map_thy f = ThyData.map (fn (Thy {axioms, defs, wrappers}) =>
+fun map_thy f = Thy.map (fn (Thy {axioms, defs, wrappers}) =>
   make_thy (f (axioms, defs, wrappers)));