# HG changeset patch
# User wenzelm
# Date 1152356086 -7200
# Node ID 7d035e26e5f9ed41cc0c830a8d6e875e4d705dd3
# Parent  058e913bac71ee10979351d011bdaff835272312
prove_witness: context;

diff -r 058e913bac71 -r 7d035e26e5f9 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Sat Jul 08 12:54:45 2006 +0200
+++ b/src/Pure/Isar/element.ML	Sat Jul 08 12:54:46 2006 +0200
@@ -38,7 +38,7 @@
   val witness_prop: witness -> term
   val witness_hyps: witness -> term list
   val assume_witness: theory -> term -> witness
-  val prove_witness: theory -> term -> tactic -> witness
+  val prove_witness: Proof.context -> term -> tactic -> witness
   val conclude_witness: witness -> thm
   val mark_witness: term -> term
   val make_witness: term -> thm -> witness
@@ -274,8 +274,8 @@
 fun assume_witness thy t =
   Witness (t, Goal.protect (Thm.assume (Thm.cterm_of thy t)));
 
-fun prove_witness thy t tac =
-  Witness (t, Goal.prove thy [] [] (Logic.protect t) (fn _ =>
+fun prove_witness ctxt t tac =
+  Witness (t, Goal.prove ctxt [] [] (Logic.protect t) (fn _ =>
     Tactic.rtac Drule.protectI 1 THEN tac));
 
 fun conclude_witness (Witness (_, th)) = Goal.norm_hhf (Goal.conclude th);