--- a/src/Provers/classical.ML Tue Nov 04 15:16:23 1997 +0100
+++ b/src/Provers/classical.ML Tue Nov 04 16:17:04 1997 +0100
@@ -26,9 +26,11 @@
signature CLASET_THY_DATA =
sig
val clasetK: string
- exception ClasetData of exn ref
- val thy_data: string * (exn * (exn -> exn) * (exn * exn -> exn) * (exn -> unit))
- val fix_methods: exn * (exn -> exn) * (exn * exn -> exn) * (exn -> unit) -> unit
+ exception ClasetData of object ref
+ val thy_data: string * (object * (object -> object) *
+ (object * object -> object) * (object -> unit))
+ val fix_methods: object * (object -> object) *
+ (object * object -> object) * (object -> unit) -> unit
end;
signature CLASSICAL_DATA =
@@ -137,15 +139,15 @@
(* data kind claset -- forward declaration *)
val clasetK = "claset";
-exception ClasetData of exn ref;
+exception ClasetData of object ref;
local
fun undef _ = raise Match;
val empty_ref = ref ERROR;
- val prep_ext_fn = ref (undef: exn -> exn);
- val merge_fn = ref (undef: exn * exn -> exn);
- val print_fn = ref (undef: exn -> unit);
+ val prep_ext_fn = ref (undef: object -> object);
+ val merge_fn = ref (undef: object * object -> object);
+ val print_fn = ref (undef: object -> unit);
val empty = ClasetData empty_ref;
fun prep_ext exn = ! prep_ext_fn exn;
--- a/src/Provers/simplifier.ML Tue Nov 04 15:16:23 1997 +0100
+++ b/src/Provers/simplifier.ML Tue Nov 04 16:17:04 1997 +0100
@@ -46,7 +46,8 @@
val merge_ss: simpset * simpset -> simpset
val prems_of_ss: simpset -> thm list
- val simpset_thy_data: string * (exn * (exn -> exn) * (exn * exn -> exn) * (exn -> unit))
+ val simpset_thy_data: string * (object * (object -> object) *
+ (object * object -> object) * (object -> unit))
val simpset_ref_of_sg: Sign.sg -> simpset ref
val simpset_ref_of: theory -> simpset ref
val simpset_of_sg: Sign.sg -> simpset
--- a/src/Pure/data.ML Tue Nov 04 15:16:23 1997 +0100
+++ b/src/Pure/data.ML Tue Nov 04 16:17:04 1997 +0100
@@ -6,6 +6,8 @@
constructors.
*)
+type object = exn;
+
signature DATA =
sig
type T
@@ -13,9 +15,10 @@
val merge: T * T -> T
val prep_ext: T -> T
val kinds: T -> string list
- val init: T -> string -> exn -> (exn -> exn) -> (exn * exn -> exn) -> (exn -> unit) -> T
- val get: T -> string -> exn
- val put: T -> string -> exn -> T
+ val init: T -> string -> object ->
+ (object -> object) -> (object * object -> object) -> (object -> unit) -> T
+ val get: T -> string -> object
+ val put: T -> string -> object -> T
val print: T -> string -> unit
end;
@@ -27,10 +30,10 @@
(* datatype T *)
datatype T = Data of
- (exn * (*value*)
- ((exn -> exn) * (*prepare extend method*)
- (exn * exn -> exn) * (*merge and prepare extend method*)
- (exn -> unit))) (*print method*)
+ (object * (*value*)
+ ((object -> object) * (*prepare extend method*)
+ (object * object -> object) * (*merge and prepare extend method*)
+ (object -> unit))) (*print method*)
Symtab.table;
val empty = Data Symtab.null;
@@ -65,9 +68,9 @@
| Some x => [(kind, x)]);
fun merge_entries [(kind, (e, mths as (ext, _, _)))] =
- (kind, (ext e handle exn => err_method "prep_ext" kind, mths))
+ (kind, (ext e handle _ => err_method "prep_ext" kind, mths))
| merge_entries [(kind, (e1, mths as (_, mrg, _))), (_, (e2, _))] =
- (kind, (mrg (e1, e2) handle exn => (err_method "merge" kind; raise exn), mths))
+ (kind, (mrg (e1, e2) handle _ => err_method "merge" kind, mths))
| merge_entries _ = sys_error "merge_entries";
val data = map (fn k => merge_entries (entry data1 k @ entry data2 k)) kinds;
@@ -95,7 +98,7 @@
fun print (Data tab) kind =
let val (e, (_, _, prt)) = lookup tab kind
- in prt e handle exn => err_method "print" kind end;
+ in prt e handle _ => err_method "print" kind end;
end;
--- a/src/Pure/pure_thy.ML Tue Nov 04 15:16:23 1997 +0100
+++ b/src/Pure/pure_thy.ML Tue Nov 04 16:17:04 1997 +0100
@@ -69,8 +69,8 @@
in
-val theorems_data:
- string * (exn * (exn -> exn) * (exn * exn -> exn) * (exn -> unit)) =
+val theorems_data: string * (object * (object -> object) *
+ (object * object -> object) * (object -> unit)) =
(theoremsK, (mk_empty (), mk_empty, mk_empty, print));
end;
--- a/src/Pure/sign.ML Tue Nov 04 15:16:23 1997 +0100
+++ b/src/Pure/sign.ML Tue Nov 04 16:17:04 1997 +0100
@@ -110,10 +110,10 @@
val add_path: string -> sg -> sg
val add_space: string * string list -> sg -> sg
val add_name: string -> sg -> sg
- val init_data: string * (exn * (exn -> exn) * (exn * exn -> exn) * (exn -> unit))
- -> sg -> sg
- val get_data: sg -> string -> exn
- val put_data: string * exn -> sg -> sg
+ val init_data: string * (object * (object -> object) *
+ (object * object -> object) * (object -> unit)) -> sg -> sg
+ val get_data: sg -> string -> object
+ val put_data: string * object -> sg -> sg
val print_data: sg -> string -> unit
val merge_refs: sg_ref * sg_ref -> sg_ref
val prep_ext: sg -> sg
--- a/src/Pure/theory.ML Tue Nov 04 15:16:23 1997 +0100
+++ b/src/Pure/theory.ML Tue Nov 04 16:17:04 1997 +0100
@@ -14,7 +14,7 @@
val rep_theory: theory ->
{sign: Sign.sg,
axioms: term Symtab.table,
- oracles: ((Sign.sg * exn -> term) * stamp) Symtab.table,
+ oracles: ((Sign.sg * object -> term) * stamp) Symtab.table,
parents: theory list,
ancestors: theory list}
val sign_of: theory -> Sign.sg
@@ -67,16 +67,16 @@
val add_trrules_i: Syntax.ast Syntax.trrule list -> theory -> theory
val add_axioms: (bstring * string) list -> theory -> theory
val add_axioms_i: (bstring * term) list -> theory -> theory
- val add_oracle: bstring * (Sign.sg * exn -> term) -> theory -> theory
+ val add_oracle: bstring * (Sign.sg * object -> term) -> theory -> theory
val add_defs: (bstring * string) list -> theory -> theory
val add_defs_i: (bstring * term) list -> theory -> theory
val add_path: string -> theory -> theory
val add_space: string * string list -> theory -> theory
val add_name: string -> theory -> theory
- val init_data: (string * (exn * (exn -> exn) * (exn * exn -> exn) * (exn -> unit))) list
- -> theory -> theory
- val get_data: theory -> string -> exn
- val put_data: string * exn -> theory -> theory
+ val init_data: (string * (object * (object -> object) *
+ (object * object -> object) * (object -> unit))) list -> theory -> theory
+ val get_data: theory -> string -> object
+ val put_data: string * object -> theory -> theory
val prep_ext: theory -> theory
val prep_ext_merge: theory list -> theory
val pre_pure: theory
@@ -93,7 +93,7 @@
Theory of {
sign: Sign.sg,
axioms: term Symtab.table,
- oracles: ((Sign.sg * exn -> term) * stamp) Symtab.table,
+ oracles: ((Sign.sg * object -> term) * stamp) Symtab.table,
parents: theory list,
ancestors: theory list};
--- a/src/Pure/thm.ML Tue Nov 04 15:16:23 1997 +0100
+++ b/src/Pure/thm.ML Tue Nov 04 16:17:04 1997 +0100
@@ -41,7 +41,7 @@
val keep_derivs : deriv_kind ref
datatype rule =
MinProof
- | Oracle of theory * string * Sign.sg * exn
+ | Oracle of theory * string * Sign.sg * object
| Axiom of theory * string
| Theorem of string
| Assume of cterm
@@ -166,7 +166,7 @@
val rewrite_cterm : bool * bool -> meta_simpset ->
(meta_simpset -> thm -> thm option) -> cterm -> thm
- val invoke_oracle : theory -> xstring -> Sign.sg * exn -> thm
+ val invoke_oracle : theory -> xstring -> Sign.sg * object -> thm
end;
structure Thm: THM =
@@ -303,7 +303,7 @@
executed in ML.*)
datatype rule =
MinProof (*for building minimal proof terms*)
- | Oracle of theory * string * Sign.sg * exn (*oracles*)
+ | Oracle of theory * string * Sign.sg * object (*oracles*)
(*Axioms/theorems*)
| Axiom of theory * string
| Theorem of string