src/Pure/thm.ML
changeset 4254 8ae7ace96c39
parent 4251 f6bd8332eb32
child 4270 957c887b89b5
     1.1 --- a/src/Pure/thm.ML	Thu Nov 20 13:00:50 1997 +0100
     1.2 +++ b/src/Pure/thm.ML	Thu Nov 20 15:06:57 1997 +0100
     1.3 @@ -88,6 +88,7 @@
     1.4                                    prop: cterm}
     1.5    val eq_thm		: thm * thm -> bool
     1.6    val sign_of_thm       : thm -> Sign.sg
     1.7 +  val transfer_sg	: Sign.sg -> thm -> thm
     1.8    val transfer		: theory -> thm -> thm
     1.9    val tpairs_of         : thm -> (term * term) list
    1.10    val prems_of          : thm -> term list
    1.11 @@ -429,18 +430,20 @@
    1.12    Sign.merge_refs (sgr1, sgr2) handle TERM (msg, _) => raise THM (msg, 0, [th1, th2]);
    1.13  
    1.14  (*transfer thm to super theory (non-destructive)*)
    1.15 -fun transfer thy thm =
    1.16 +fun transfer_sg sign' thm =
    1.17    let
    1.18      val Thm {sign_ref, der, maxidx, shyps, hyps, prop} = thm;
    1.19      val sign = Sign.deref sign_ref;
    1.20 -    val sign' = #sign (rep_theory thy);
    1.21    in
    1.22 -    if Sign.subsig (sign, sign') then
    1.23 +    if Sign.eq_sg (sign, sign') then thm
    1.24 +    else if Sign.subsig (sign, sign') then
    1.25        Thm {sign_ref = Sign.self_ref sign', der = der, maxidx = maxidx,
    1.26          shyps = shyps, hyps = hyps, prop = prop}
    1.27      else raise THM ("transfer: not a super theory", 0, [thm])
    1.28    end;
    1.29  
    1.30 +val transfer = transfer_sg o sign_of;
    1.31 +
    1.32  (*maps object-rule to tpairs*)
    1.33  fun tpairs_of (Thm {prop, ...}) = #1 (Logic.strip_flexpairs prop);
    1.34