--- a/src/Pure/theory.ML Thu Sep 18 14:06:58 2008 +0200
+++ b/src/Pure/theory.ML Thu Sep 18 19:39:44 2008 +0200
@@ -2,7 +2,7 @@
ID: $Id$
Author: Lawrence C Paulson and Markus Wenzel
-Logical theory content: axioms, definitions, oracles.
+Logical theory content: axioms, definitions, and begin/end wrappers.
*)
signature THEORY =
@@ -22,8 +22,6 @@
val requires: theory -> string -> string -> unit
val axiom_space: theory -> NameSpace.T
val axiom_table: theory -> term Symtab.table
- val oracle_space: theory -> NameSpace.T
- val oracle_table: theory -> ((theory * Object.T -> term) * stamp) Symtab.table
val axioms_of: theory -> (string * term) list
val all_axioms_of: theory -> (string * term) list
val defs_of: theory -> Defs.T
@@ -39,7 +37,6 @@
val add_finals: bool -> string list -> theory -> theory
val add_finals_i: bool -> term list -> theory -> theory
val specify_const: Properties.T -> (Name.binding * typ) * mixfix -> theory -> term * theory
- val add_oracle: bstring * (theory * Object.T -> term) -> theory -> theory
end
structure Theory: THEORY =
@@ -86,55 +83,41 @@
datatype thy = Thy of
{axioms: term NameSpace.table,
defs: Defs.T,
- oracles: ((theory * Object.T -> term) * stamp) NameSpace.table,
wrappers: wrapper list * wrapper list};
-fun make_thy (axioms, defs, oracles, wrappers) =
- Thy {axioms = axioms, defs = defs, oracles = oracles, wrappers = wrappers};
+fun make_thy (axioms, defs, wrappers) = Thy {axioms = axioms, defs = defs, wrappers = wrappers};
fun err_dup_axm dup = error ("Duplicate axiom: " ^ quote dup);
-fun err_dup_ora dup = error ("Duplicate oracle: " ^ quote dup);
structure ThyData = TheoryDataFun
(
type T = thy;
- val empty = make_thy (NameSpace.empty_table, Defs.empty, NameSpace.empty_table, ([], []));
+ val empty = make_thy (NameSpace.empty_table, Defs.empty, ([], []));
val copy = I;
- fun extend (Thy {axioms, defs, oracles, wrappers}) =
- make_thy (NameSpace.empty_table, defs, oracles, wrappers);
+ fun extend (Thy {axioms, defs, wrappers}) = make_thy (NameSpace.empty_table, defs, wrappers);
fun merge pp (thy1, thy2) =
let
- val Thy {axioms = _, defs = defs1, oracles = oracles1, wrappers = (bgs1, ens1)} = thy1;
- val Thy {axioms = _, defs = defs2, oracles = oracles2, wrappers = (bgs2, ens2)} = thy2;
+ val Thy {axioms = _, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
+ val Thy {axioms = _, defs = defs2, wrappers = (bgs2, ens2)} = thy2;
val axioms' = NameSpace.empty_table;
val defs' = Defs.merge pp (defs1, defs2);
- val oracles' = NameSpace.merge_tables (eq_snd (op =)) (oracles1, oracles2)
- handle Symtab.DUP dup => err_dup_ora dup;
val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2);
val ens' = Library.merge (eq_snd op =) (ens1, ens2);
- in make_thy (axioms', defs', oracles', (bgs', ens')) end;
+ in make_thy (axioms', defs', (bgs', ens')) end;
);
fun rep_theory thy = ThyData.get thy |> (fn Thy args => args);
-fun map_thy f = ThyData.map (fn (Thy {axioms, defs, oracles, wrappers}) =>
- make_thy (f (axioms, defs, oracles, wrappers)));
+fun map_thy f = ThyData.map (fn (Thy {axioms, defs, wrappers}) =>
+ make_thy (f (axioms, defs, wrappers)));
-fun map_axioms f = map_thy
- (fn (axioms, defs, oracles, wrappers) => (f axioms, defs, oracles, wrappers));
-
-fun map_defs f = map_thy
- (fn (axioms, defs, oracles, wrappers) => (axioms, f defs, oracles, wrappers));
-
-fun map_oracles f = map_thy
- (fn (axioms, defs, oracles, wrappers) => (axioms, defs, f oracles, wrappers));
-
-fun map_wrappers f = map_thy
- (fn (axioms, defs, oracles, wrappers) => (axioms, defs, oracles, f wrappers));
+fun map_axioms f = map_thy (fn (axioms, defs, wrappers) => (f axioms, defs, wrappers));
+fun map_defs f = map_thy (fn (axioms, defs, wrappers) => (axioms, f defs, wrappers));
+fun map_wrappers f = map_thy (fn (axioms, defs, wrappers) => (axioms, defs, f wrappers));
(* basic operations *)
@@ -142,9 +125,6 @@
val axiom_space = #1 o #axioms o rep_theory;
val axiom_table = #2 o #axioms o rep_theory;
-val oracle_space = #1 o #oracles o rep_theory;
-val oracle_table = #2 o #oracles o rep_theory;
-
val axioms_of = Symtab.dest o #2 o #axioms o rep_theory;
fun all_axioms_of thy = maps axioms_of (thy :: ancestors_of thy);
@@ -323,13 +303,4 @@
end;
-
-
-(** add oracle **)
-
-fun add_oracle (bname, oracle) thy = thy |> map_oracles (fn oracles =>
- NameSpace.extend_table (Sign.naming_of thy) [(bname, (oracle, stamp ()))] oracles
- handle Symtab.DUP dup => err_dup_ora dup);
-
end;
-