tuned;

--- a/src/Pure/Thy/term_style.ML	Sun Mar 20 22:26:43 2011 +0100
+++ b/src/Pure/Thy/term_style.ML	Sun Mar 20 22:47:08 2011 +0100
@@ -19,7 +19,7 @@
 fun err_dup_style name =
   error ("Duplicate declaration of antiquote style: " ^ quote name);
 
-structure StyleData = Theory_Data
+structure Styles = Theory_Data
 (
   type T = ((Proof.context -> term -> term) parser * stamp) Symtab.table;
   val empty = Symtab.empty;
@@ -32,12 +32,12 @@
 (* accessors *)
 
 fun the_style thy name =
-  (case Symtab.lookup (StyleData.get thy) name of
+  (case Symtab.lookup (Styles.get thy) name of
     NONE => error ("Unknown antiquote style: " ^ quote name)
   | SOME (style, _) => style);
 
 fun setup name style thy =
-  StyleData.map (Symtab.update_new (name, (style, stamp ()))) thy
+  Styles.map (Symtab.update_new (name, (style, stamp ()))) thy
     handle Symtab.DUP _ => err_dup_style name;
 
 

--- 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)));