# HG changeset patch
# User wenzelm
# Date 1197651368 -3600
# Node ID 04b67ee7332746f40a5b3f4b78e43cc2f2c471f8
# Parent  baa627b6f96242a1c7d17ea7c9826c5301afa810
added close_witness;

diff -r baa627b6f962 -r 04b67ee73327 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Thu Dec 13 22:35:45 2007 +0100
+++ b/src/Pure/Isar/element.ML	Fri Dec 14 17:56:08 2007 +0100
@@ -45,6 +45,7 @@
   val witness_hyps: witness -> term list
   val assume_witness: theory -> term -> witness
   val prove_witness: Proof.context -> term -> tactic -> witness
+  val close_witness: witness -> witness
   val conclude_witness: witness -> thm
   val mark_witness: term -> term
   val make_witness: term -> thm -> witness
@@ -293,6 +294,8 @@
   Witness (t, Goal.close_result (Goal.prove ctxt [] [] (Logic.protect t) (fn _ =>
     Tactic.rtac Drule.protectI 1 THEN tac)));
 
+val close_witness = map_witness (fn (t, th) => (t, Goal.close_result th));
+
 fun conclude_witness (Witness (_, th)) =
   Goal.close_result (MetaSimplifier.norm_hhf_protect (Goal.conclude th));