src/Pure/thm.ML
changeset 4124 1af16493c57f
parent 4116 42606637f87f
child 4182 47067b5db7ef
     1.1 --- a/src/Pure/thm.ML	Tue Nov 04 15:16:23 1997 +0100
     1.2 +++ b/src/Pure/thm.ML	Tue Nov 04 16:17:04 1997 +0100
     1.3 @@ -41,7 +41,7 @@
     1.4    val keep_derivs       : deriv_kind ref
     1.5    datatype rule = 
     1.6        MinProof                          
     1.7 -    | Oracle of theory * string * Sign.sg * exn
     1.8 +    | Oracle of theory * string * Sign.sg * object
     1.9      | Axiom               of theory * string
    1.10      | Theorem             of string       
    1.11      | Assume              of cterm
    1.12 @@ -166,7 +166,7 @@
    1.13    val rewrite_cterm     : bool * bool -> meta_simpset ->
    1.14                            (meta_simpset -> thm -> thm option) -> cterm -> thm
    1.15  
    1.16 -  val invoke_oracle     : theory -> xstring -> Sign.sg * exn -> thm
    1.17 +  val invoke_oracle     : theory -> xstring -> Sign.sg * object -> thm
    1.18  end;
    1.19  
    1.20  structure Thm: THM =
    1.21 @@ -303,7 +303,7 @@
    1.22    executed in ML.*)
    1.23  datatype rule = 
    1.24      MinProof                            (*for building minimal proof terms*)
    1.25 -  | Oracle              of theory * string * Sign.sg * exn       (*oracles*)
    1.26 +  | Oracle              of theory * string * Sign.sg * object       (*oracles*)
    1.27  (*Axioms/theorems*)
    1.28    | Axiom               of theory * string
    1.29    | Theorem             of string