# HG changeset patch
# User wenzelm
# Date 880034817 -3600
# Node ID 8ae7ace96c391870cf582de6fa6f76cb982283aa
# Parent  901f690e3a58a84a0893ada23eec0677745573c3
added transfer_sg;

diff -r 901f690e3a58 -r 8ae7ace96c39 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Nov 20 13:00:50 1997 +0100
+++ b/src/Pure/thm.ML	Thu Nov 20 15:06:57 1997 +0100
@@ -88,6 +88,7 @@
                                   prop: cterm}
   val eq_thm		: thm * thm -> bool
   val sign_of_thm       : thm -> Sign.sg
+  val transfer_sg	: Sign.sg -> thm -> thm
   val transfer		: theory -> thm -> thm
   val tpairs_of         : thm -> (term * term) list
   val prems_of          : thm -> term list
@@ -429,18 +430,20 @@
   Sign.merge_refs (sgr1, sgr2) handle TERM (msg, _) => raise THM (msg, 0, [th1, th2]);
 
 (*transfer thm to super theory (non-destructive)*)
-fun transfer thy thm =
+fun transfer_sg sign' thm =
   let
     val Thm {sign_ref, der, maxidx, shyps, hyps, prop} = thm;
     val sign = Sign.deref sign_ref;
-    val sign' = #sign (rep_theory thy);
   in
-    if Sign.subsig (sign, sign') then
+    if Sign.eq_sg (sign, sign') then thm
+    else if Sign.subsig (sign, sign') then
       Thm {sign_ref = Sign.self_ref sign', der = der, maxidx = maxidx,
         shyps = shyps, hyps = hyps, prop = prop}
     else raise THM ("transfer: not a super theory", 0, [thm])
   end;
 
+val transfer = transfer_sg o sign_of;
+
 (*maps object-rule to tpairs*)
 fun tpairs_of (Thm {prop, ...}) = #1 (Logic.strip_flexpairs prop);