added transfer: theory -> thm -> thm;
authorwenzelm
Thu Oct 16 14:00:20 1997 +0200 (1997-10-16)
changeset 3895b2463861c86a
parent 3894 8b9f0bc6dc1a
child 3896 ee8ebb74ec00
added transfer: theory -> thm -> thm;
src/Pure/thm.ML
     1.1 --- a/src/Pure/thm.ML	Thu Oct 16 13:45:27 1997 +0200
     1.2 +++ b/src/Pure/thm.ML	Thu Oct 16 14:00:20 1997 +0200
     1.3 @@ -36,8 +36,6 @@
     1.4      Sign.sg * (indexname -> typ option) * (indexname -> sort option) ->
     1.5      string list -> bool -> string * typ -> cterm * (indexname * typ) list
     1.6  
     1.7 -  (*theories*)
     1.8 -
     1.9    (*proof terms [must DUPLICATE declaration as a specification]*)
    1.10    datatype deriv_kind = MinDeriv | ThmDeriv | FullDeriv;
    1.11    val keep_derivs       : deriv_kind ref
    1.12 @@ -89,6 +87,7 @@
    1.13                                    shyps: sort list, hyps: cterm list, 
    1.14                                    prop: cterm}
    1.15    val stamps_of_thm     : thm -> string ref list
    1.16 +  val transfer		: theory -> thm -> thm
    1.17    val tpairs_of         : thm -> (term * term) list
    1.18    val prems_of          : thm -> term list
    1.19    val nprems_of         : thm -> int
    1.20 @@ -413,6 +412,17 @@
    1.21    Sign.merge (pairself (#sign o rep_thm) (th1, th2))
    1.22      handle TERM (msg, _) => raise THM (msg, 0, [th1, th2]);
    1.23  
    1.24 +(*transfer thm to super theory*)
    1.25 +fun transfer thy thm =
    1.26 +  let
    1.27 +    val Thm {sign, der, maxidx, shyps, hyps, prop} = thm;
    1.28 +    val sign' = #sign (rep_theory thy);
    1.29 +  in
    1.30 +    if Sign.subsig (sign, sign') then
    1.31 +      Thm {sign = sign', der = der, maxidx = maxidx,
    1.32 +        shyps = shyps, hyps = hyps, prop = prop}
    1.33 +    else raise THM ("transfer: not a super theory", 0, [thm])
    1.34 +  end;
    1.35  
    1.36  (*maps object-rule to tpairs*)
    1.37  fun tpairs_of (Thm {prop, ...}) = #1 (Logic.strip_flexpairs prop);