# HG changeset patch
# User ballarin
# Date 1152609429 -7200
# Node ID 19c7361db4a388fc5bd6c1ab3b79810c5dd3ff4b
# Parent  26bac504ef90b8a955a2a8fcb4031bd41c4f2930
New function transfer_witness lifting Thm.transfer to witnesses.

diff -r 26bac504ef90 -r 19c7361db4a3 src/Pure/Isar/element.ML
--- 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