src/Pure/Isar/element.ML

   val prove_witness: Proof.context -> term -> tactic -> witness
   val conclude_witness: witness -> thm
   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
   val rename_term: (string * (string * mixfix option)) list -> term -> term
   val rename_thm: (string * (string * mixfix option)) list -> thm -> thm

 
 fun make_witness t th = Witness (t, th);
 
 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
       (PRECISE_CONJUNCTS ~1 (ALLGOALS
         (PRECISE_CONJUNCTS ~1 (TRYALL (Tactic.rtac Drule.protectI))))))))));