src/Pure/theory.ML
changeset 42016 3b6826b3ed37
parent 39134 917b4b6ba3d2
child 42360 da8817d01e7c
equal deleted inserted replaced
42015:7b6e72a1b7dd 42016:3b6826b3ed37
    82   defs: Defs.T,
    82   defs: Defs.T,
    83   wrappers: wrapper list * wrapper list};
    83   wrappers: wrapper list * wrapper list};
    84 
    84 
    85 fun make_thy (axioms, defs, wrappers) = Thy {axioms = axioms, defs = defs, wrappers = wrappers};
    85 fun make_thy (axioms, defs, wrappers) = Thy {axioms = axioms, defs = defs, wrappers = wrappers};
    86 
    86 
    87 structure ThyData = Theory_Data_PP
    87 structure Thy = Theory_Data_PP
    88 (
    88 (
    89   type T = thy;
    89   type T = thy;
    90   val empty_axioms = Name_Space.empty_table "axiom" : term Name_Space.table;
    90   val empty_axioms = Name_Space.empty_table "axiom" : term Name_Space.table;
    91   val empty = make_thy (empty_axioms, Defs.empty, ([], []));
    91   val empty = make_thy (empty_axioms, Defs.empty, ([], []));
    92 
    92 
   102       val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2);
   102       val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2);
   103       val ens' = Library.merge (eq_snd op =) (ens1, ens2);
   103       val ens' = Library.merge (eq_snd op =) (ens1, ens2);
   104     in make_thy (axioms', defs', (bgs', ens')) end;
   104     in make_thy (axioms', defs', (bgs', ens')) end;
   105 );
   105 );
   106 
   106 
   107 fun rep_theory thy = ThyData.get thy |> (fn Thy args => args);
   107 fun rep_theory thy = Thy.get thy |> (fn Thy args => args);
   108 
   108 
   109 fun map_thy f = ThyData.map (fn (Thy {axioms, defs, wrappers}) =>
   109 fun map_thy f = Thy.map (fn (Thy {axioms, defs, wrappers}) =>
   110   make_thy (f (axioms, defs, wrappers)));
   110   make_thy (f (axioms, defs, wrappers)));
   111 
   111 
   112 
   112 
   113 fun map_axioms f = map_thy (fn (axioms, defs, wrappers) => (f axioms, defs, wrappers));
   113 fun map_axioms f = map_thy (fn (axioms, defs, wrappers) => (f axioms, defs, wrappers));
   114 fun map_defs f = map_thy (fn (axioms, defs, wrappers) => (axioms, f defs, wrappers));
   114 fun map_defs f = map_thy (fn (axioms, defs, wrappers) => (axioms, f defs, wrappers));