# HG changeset patch
# User wenzelm
# Date 877003220 -7200
# Node ID b2463861c86ae6b92d40a4d89e01d3ecaa1e8361
# Parent  8b9f0bc6dc1aa780bae5ff8e1ba1cd8a672226ce
added transfer: theory -> thm -> thm;

diff -r 8b9f0bc6dc1a -r b2463861c86a src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Oct 16 13:45:27 1997 +0200
+++ b/src/Pure/thm.ML	Thu Oct 16 14:00:20 1997 +0200
@@ -36,8 +36,6 @@
     Sign.sg * (indexname -> typ option) * (indexname -> sort option) ->
     string list -> bool -> string * typ -> cterm * (indexname * typ) list
 
-  (*theories*)
-
   (*proof terms [must DUPLICATE declaration as a specification]*)
   datatype deriv_kind = MinDeriv | ThmDeriv | FullDeriv;
   val keep_derivs       : deriv_kind ref
@@ -89,6 +87,7 @@
                                   shyps: sort list, hyps: cterm list, 
                                   prop: cterm}
   val stamps_of_thm     : thm -> string ref list
+  val transfer		: theory -> thm -> thm
   val tpairs_of         : thm -> (term * term) list
   val prems_of          : thm -> term list
   val nprems_of         : thm -> int
@@ -413,6 +412,17 @@
   Sign.merge (pairself (#sign o rep_thm) (th1, th2))
     handle TERM (msg, _) => raise THM (msg, 0, [th1, th2]);
 
+(*transfer thm to super theory*)
+fun transfer thy thm =
+  let
+    val Thm {sign, der, maxidx, shyps, hyps, prop} = thm;
+    val sign' = #sign (rep_theory thy);
+  in
+    if Sign.subsig (sign, sign') then
+      Thm {sign = sign', der = der, maxidx = maxidx,
+        shyps = shyps, hyps = hyps, prop = prop}
+    else raise THM ("transfer: not a super theory", 0, [thm])
+  end;
 
 (*maps object-rule to tpairs*)
 fun tpairs_of (Thm {prop, ...}) = #1 (Logic.strip_flexpairs prop);