tuned;
authorwenzelm
Sun Mar 20 22:47:08 2011 +0100 (2011-03-20)
changeset 420163b6826b3ed37
parent 42015 7b6e72a1b7dd
child 42017 0d4bedb25fc9
tuned;
src/Pure/Thy/term_style.ML
src/Pure/theory.ML
     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