deriv: eliminated references to theory;
authorwenzelm
Thu Nov 06 16:41:08 1997 +0100 (1997-11-06)
changeset 418247067b5db7ef
parent 4181 fcc8b47e4c49
child 4183 706902a9abdd
deriv: eliminated references to theory;
src/Pure/thm.ML
     1.1 --- a/src/Pure/thm.ML	Thu Nov 06 16:40:45 1997 +0100
     1.2 +++ b/src/Pure/thm.ML	Thu Nov 06 16:41:08 1997 +0100
     1.3 @@ -41,8 +41,8 @@
     1.4    val keep_derivs       : deriv_kind ref
     1.5    datatype rule = 
     1.6        MinProof                          
     1.7 -    | Oracle of theory * string * Sign.sg * object
     1.8 -    | Axiom               of theory * string
     1.9 +    | Oracle		  of string * Sign.sg * object
    1.10 +    | Axiom               of string
    1.11      | Theorem             of string       
    1.12      | Assume              of cterm
    1.13      | Implies_intr        of cterm
    1.14 @@ -67,7 +67,7 @@
    1.15      | Instantiate         of (indexname * ctyp) list * (cterm * cterm) list
    1.16      | Bicompose           of bool * bool * int * int * Envir.env
    1.17      | Flexflex_rule       of Envir.env            
    1.18 -    | Class_triv          of theory * class       
    1.19 +    | Class_triv          of class       
    1.20      | VarifyT
    1.21      | FreezeT
    1.22      | RewriteC            of cterm
    1.23 @@ -303,9 +303,9 @@
    1.24    executed in ML.*)
    1.25  datatype rule = 
    1.26      MinProof                            (*for building minimal proof terms*)
    1.27 -  | Oracle              of theory * string * Sign.sg * object       (*oracles*)
    1.28 +  | Oracle              of string * Sign.sg * object       (*oracles*)
    1.29  (*Axioms/theorems*)
    1.30 -  | Axiom               of theory * string
    1.31 +  | Axiom               of string
    1.32    | Theorem             of string
    1.33  (*primitive inferences and compound versions of them*)
    1.34    | Assume              of cterm
    1.35 @@ -335,7 +335,7 @@
    1.36    | Bicompose           of bool * bool * int * int * Envir.env
    1.37    | Flexflex_rule       of Envir.env            (*identifies unifier chosen*)
    1.38  (*other derived rules*)
    1.39 -  | Class_triv          of theory * class
    1.40 +  | Class_triv          of class
    1.41    | VarifyT
    1.42    | FreezeT
    1.43  (*for the simplifier*)
    1.44 @@ -585,7 +585,7 @@
    1.45            in case Symtab.lookup (axioms, name) of
    1.46                  Some t => fix_shyps [] []
    1.47                             (Thm {sign_ref = Sign.self_ref sign,
    1.48 -                                 der = infer_derivs (Axiom(theory,name), []),
    1.49 +                                 der = infer_derivs (Axiom name, []),
    1.50                                   maxidx = maxidx_of_term t,
    1.51                                   shyps = [], 
    1.52                                   hyps = [], 
    1.53 @@ -614,7 +614,7 @@
    1.54  fun name_of_thm (Thm {der, ...}) =
    1.55    (case der of
    1.56      Join (Theorem name, _) => name
    1.57 -  | Join (Axiom (_, name), _) => name
    1.58 +  | Join (Axiom name, _) => name
    1.59    | _ => "");
    1.60  
    1.61  
    1.62 @@ -1095,7 +1095,7 @@
    1.63    in
    1.64      fix_shyps [] []
    1.65        (Thm {sign_ref = sign_ref, 
    1.66 -            der = infer_derivs (Class_triv(thy,c), []), 
    1.67 +            der = infer_derivs (Class_triv c, []), 
    1.68              maxidx = maxidx, 
    1.69              shyps = [], 
    1.70              hyps = [], 
    1.71 @@ -2024,7 +2024,7 @@
    1.72            raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
    1.73          else fix_shyps [] []
    1.74            (Thm {sign_ref = sign_ref', 
    1.75 -            der = Join (Oracle (thy, name, sign, exn), []),
    1.76 +            der = Join (Oracle (name, sign, exn), []),
    1.77              maxidx = maxidx,
    1.78              shyps = [], 
    1.79              hyps = [],