src/Pure/Isar/element.ML
changeset 19931 fb32b43e7f80
parent 19897 fe661eb3b0e7
child 20007 8f9e6255108e
     1.1 --- a/src/Pure/Isar/element.ML	Tue Jun 20 14:51:59 2006 +0200
     1.2 +++ b/src/Pure/Isar/element.ML	Tue Jun 20 15:53:44 2006 +0200
     1.3 @@ -42,6 +42,7 @@
     1.4    val conclude_witness: witness -> thm
     1.5    val mark_witness: term -> term
     1.6    val make_witness: term -> thm -> witness
     1.7 +  val dest_witness: witness -> term * thm
     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 @@ -283,6 +284,8 @@
    1.12  
    1.13  fun make_witness t th = Witness (t, th);
    1.14  
    1.15 +fun dest_witness (Witness w) = w;
    1.16 +
    1.17  val refine_witness =
    1.18    Proof.refine (Method.Basic (K (Method.RAW_METHOD
    1.19      (K (ALLGOALS