1.1 --- a/src/Pure/Thy/term_style.ML Sun Mar 20 22:26:43 2011 +0100
1.2 +++ b/src/Pure/Thy/term_style.ML Sun Mar 20 22:47:08 2011 +0100
1.3 @@ -19,7 +19,7 @@
1.4 fun err_dup_style name =
1.5 error ("Duplicate declaration of antiquote style: " ^ quote name);
1.6
1.7 -structure StyleData = Theory_Data
1.8 +structure Styles = Theory_Data
1.9 (
1.10 type T = ((Proof.context -> term -> term) parser * stamp) Symtab.table;
1.11 val empty = Symtab.empty;
1.12 @@ -32,12 +32,12 @@
1.13 (* accessors *)
1.14
1.15 fun the_style thy name =
1.16 - (case Symtab.lookup (StyleData.get thy) name of
1.17 + (case Symtab.lookup (Styles.get thy) name of
1.18 NONE => error ("Unknown antiquote style: " ^ quote name)
1.19 | SOME (style, _) => style);
1.20
1.21 fun setup name style thy =
1.22 - StyleData.map (Symtab.update_new (name, (style, stamp ()))) thy
1.23 + Styles.map (Symtab.update_new (name, (style, stamp ()))) thy
1.24 handle Symtab.DUP _ => err_dup_style name;
1.25
1.26
2.1 --- a/src/Pure/theory.ML Sun Mar 20 22:26:43 2011 +0100
2.2 +++ b/src/Pure/theory.ML Sun Mar 20 22:47:08 2011 +0100
2.3 @@ -84,7 +84,7 @@
2.4
2.5 fun make_thy (axioms, defs, wrappers) = Thy {axioms = axioms, defs = defs, wrappers = wrappers};
2.6
2.7 -structure ThyData = Theory_Data_PP
2.8 +structure Thy = Theory_Data_PP
2.9 (
2.10 type T = thy;
2.11 val empty_axioms = Name_Space.empty_table "axiom" : term Name_Space.table;
2.12 @@ -104,9 +104,9 @@
2.13 in make_thy (axioms', defs', (bgs', ens')) end;
2.14 );
2.15
2.16 -fun rep_theory thy = ThyData.get thy |> (fn Thy args => args);
2.17 +fun rep_theory thy = Thy.get thy |> (fn Thy args => args);
2.18
2.19 -fun map_thy f = ThyData.map (fn (Thy {axioms, defs, wrappers}) =>
2.20 +fun map_thy f = Thy.map (fn (Thy {axioms, defs, wrappers}) =>
2.21 make_thy (f (axioms, defs, wrappers)));
2.22
2.23