New function transfer_witness lifting Thm.transfer to witnesses.

--- a/src/Pure/Isar/element.ML	Tue Jul 11 00:43:54 2006 +0200
+++ b/src/Pure/Isar/element.ML	Tue Jul 11 11:17:09 2006 +0200
@@ -43,6 +43,7 @@
   val mark_witness: term -> term
   val make_witness: term -> thm -> witness
   val dest_witness: witness -> term * thm
+  val transfer_witness: theory -> witness -> witness
   val refine_witness: Proof.state -> Proof.state Seq.seq
   val rename: (string * (string * mixfix option)) list -> string -> string
   val rename_var: (string * (string * mixfix option)) list -> string * mixfix -> string * mixfix
@@ -286,6 +287,8 @@
 
 fun dest_witness (Witness w) = w;
 
+fun transfer_witness thy (Witness (t, th)) = Witness (t, Thm.transfer thy th);
+
 val refine_witness =
   Proof.refine (Method.Basic (K (Method.RAW_METHOD
     (K (ALLGOALS