# HG changeset patch
# User wenzelm
# Date 878830868 -3600
# Node ID 47067b5db7efc9d056c8abd6d1e3deb73b7043d0
# Parent  fcc8b47e4c4909f41e78c4ec5ce0f28b96376e4c
deriv: eliminated references to theory;

diff -r fcc8b47e4c49 -r 47067b5db7ef src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Nov 06 16:40:45 1997 +0100
+++ b/src/Pure/thm.ML	Thu Nov 06 16:41:08 1997 +0100
@@ -41,8 +41,8 @@
   val keep_derivs       : deriv_kind ref
   datatype rule = 
       MinProof                          
-    | Oracle of theory * string * Sign.sg * object
-    | Axiom               of theory * string
+    | Oracle		  of string * Sign.sg * object
+    | Axiom               of string
     | Theorem             of string       
     | Assume              of cterm
     | Implies_intr        of cterm
@@ -67,7 +67,7 @@
     | Instantiate         of (indexname * ctyp) list * (cterm * cterm) list
     | Bicompose           of bool * bool * int * int * Envir.env
     | Flexflex_rule       of Envir.env            
-    | Class_triv          of theory * class       
+    | Class_triv          of class       
     | VarifyT
     | FreezeT
     | RewriteC            of cterm
@@ -303,9 +303,9 @@
   executed in ML.*)
 datatype rule = 
     MinProof                            (*for building minimal proof terms*)
-  | Oracle              of theory * string * Sign.sg * object       (*oracles*)
+  | Oracle              of string * Sign.sg * object       (*oracles*)
 (*Axioms/theorems*)
-  | Axiom               of theory * string
+  | Axiom               of string
   | Theorem             of string
 (*primitive inferences and compound versions of them*)
   | Assume              of cterm
@@ -335,7 +335,7 @@
   | Bicompose           of bool * bool * int * int * Envir.env
   | Flexflex_rule       of Envir.env            (*identifies unifier chosen*)
 (*other derived rules*)
-  | Class_triv          of theory * class
+  | Class_triv          of class
   | VarifyT
   | FreezeT
 (*for the simplifier*)
@@ -585,7 +585,7 @@
           in case Symtab.lookup (axioms, name) of
                 Some t => fix_shyps [] []
                            (Thm {sign_ref = Sign.self_ref sign,
-                                 der = infer_derivs (Axiom(theory,name), []),
+                                 der = infer_derivs (Axiom name, []),
                                  maxidx = maxidx_of_term t,
                                  shyps = [], 
                                  hyps = [], 
@@ -614,7 +614,7 @@
 fun name_of_thm (Thm {der, ...}) =
   (case der of
     Join (Theorem name, _) => name
-  | Join (Axiom (_, name), _) => name
+  | Join (Axiom name, _) => name
   | _ => "");
 
 
@@ -1095,7 +1095,7 @@
   in
     fix_shyps [] []
       (Thm {sign_ref = sign_ref, 
-            der = infer_derivs (Class_triv(thy,c), []), 
+            der = infer_derivs (Class_triv c, []), 
             maxidx = maxidx, 
             shyps = [], 
             hyps = [], 
@@ -2024,7 +2024,7 @@
           raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
         else fix_shyps [] []
           (Thm {sign_ref = sign_ref', 
-            der = Join (Oracle (thy, name, sign, exn), []),
+            der = Join (Oracle (name, sign, exn), []),
             maxidx = maxidx,
             shyps = [], 
             hyps = [],