# HG changeset patch # User wenzelm # Date 1300657628 -3600 # Node ID 3b6826b3ed37c034881a89326138bb1a41506af6 # Parent 7b6e72a1b7dd265b2a36c2aa473c8b1d571e3576 tuned; diff -r 7b6e72a1b7dd -r 3b6826b3ed37 src/Pure/Thy/term_style.ML --- 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; diff -r 7b6e72a1b7dd -r 3b6826b3ed37 src/Pure/theory.ML --- 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)));