# HG changeset patch
# User wenzelm
# Date 878656624 -3600
# Node ID 1af16493c57f48155333c7a9500d2dacfdd76937
# Parent  9600dd68d35b2e55079a7ed2eb80e6d26b1987d4
type object = exn (enhance readability);

diff -r 9600dd68d35b -r 1af16493c57f src/Provers/classical.ML
--- 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;
diff -r 9600dd68d35b -r 1af16493c57f src/Provers/simplifier.ML
--- 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
diff -r 9600dd68d35b -r 1af16493c57f src/Pure/data.ML
--- 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;
diff -r 9600dd68d35b -r 1af16493c57f src/Pure/pure_thy.ML
--- 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;
diff -r 9600dd68d35b -r 1af16493c57f src/Pure/sign.ML
--- 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
diff -r 9600dd68d35b -r 1af16493c57f src/Pure/theory.ML
--- 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};
 
diff -r 9600dd68d35b -r 1af16493c57f src/Pure/thm.ML
--- 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