# HG changeset patch
# User wenzelm
# Date 897049794 -7200
# Node ID 4c74267cfa0cdbc3fa629022b4887ea84479eee7
# Parent  28fe46a570d7e219b0231f967314f649f26ea9d4
Object.T;

diff -r 28fe46a570d7 -r 4c74267cfa0c src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Jun 05 14:29:33 1998 +0200
+++ b/src/Pure/thm.ML	Fri Jun 05 14:29:54 1998 +0200
@@ -44,7 +44,7 @@
   val keep_derivs       : deriv_kind ref
   datatype rule = 
       MinProof                          
-    | Oracle		  of string * Sign.sg * object
+    | Oracle		  of string * Sign.sg * Object.T
     | Axiom               of string
     | Theorem             of string       
     | Assume              of cterm
@@ -172,7 +172,7 @@
   val rewrite_cterm     : bool * bool * bool -> meta_simpset ->
                           (meta_simpset -> thm -> thm option) -> cterm -> thm
 
-  val invoke_oracle     : theory -> xstring -> Sign.sg * object -> thm
+  val invoke_oracle     : theory -> xstring -> Sign.sg * Object.T -> thm
 end;
 
 structure Thm: THM =
@@ -298,7 +298,7 @@
   executed in ML.*)
 datatype rule = 
     MinProof                            (*for building minimal proof terms*)
-  | Oracle              of string * Sign.sg * object       (*oracles*)
+  | Oracle              of string * Sign.sg * Object.T       (*oracles*)
 (*Axioms/theorems*)
   | Axiom               of string
   | Theorem             of string