New function transfer_witness lifting Thm.transfer to witnesses.
authorballarin
Tue Jul 11 11:17:09 2006 +0200 (2006-07-11)
changeset 2006819c7361db4a3
parent 20067 26bac504ef90
child 20069 77a6b62418bb
New function transfer_witness lifting Thm.transfer to witnesses.
src/Pure/Isar/element.ML
     1.1 --- a/src/Pure/Isar/element.ML	Tue Jul 11 00:43:54 2006 +0200
     1.2 +++ b/src/Pure/Isar/element.ML	Tue Jul 11 11:17:09 2006 +0200
     1.3 @@ -43,6 +43,7 @@
     1.4    val mark_witness: term -> term
     1.5    val make_witness: term -> thm -> witness
     1.6    val dest_witness: witness -> term * thm
     1.7 +  val transfer_witness: theory -> witness -> witness
     1.8    val refine_witness: Proof.state -> Proof.state Seq.seq
     1.9    val rename: (string * (string * mixfix option)) list -> string -> string
    1.10    val rename_var: (string * (string * mixfix option)) list -> string * mixfix -> string * mixfix
    1.11 @@ -286,6 +287,8 @@
    1.12  
    1.13  fun dest_witness (Witness w) = w;
    1.14  
    1.15 +fun transfer_witness thy (Witness (t, th)) = Witness (t, Thm.transfer thy th);
    1.16 +
    1.17  val refine_witness =
    1.18    Proof.refine (Method.Basic (K (Method.RAW_METHOD
    1.19      (K (ALLGOALS