src/Pure/Isar/element.ML
changeset 20058 7d035e26e5f9
parent 20007 8f9e6255108e
child 20068 19c7361db4a3
     1.1 --- a/src/Pure/Isar/element.ML	Sat Jul 08 12:54:45 2006 +0200
     1.2 +++ b/src/Pure/Isar/element.ML	Sat Jul 08 12:54:46 2006 +0200
     1.3 @@ -38,7 +38,7 @@
     1.4    val witness_prop: witness -> term
     1.5    val witness_hyps: witness -> term list
     1.6    val assume_witness: theory -> term -> witness
     1.7 -  val prove_witness: theory -> term -> tactic -> witness
     1.8 +  val prove_witness: Proof.context -> term -> tactic -> witness
     1.9    val conclude_witness: witness -> thm
    1.10    val mark_witness: term -> term
    1.11    val make_witness: term -> thm -> witness
    1.12 @@ -274,8 +274,8 @@
    1.13  fun assume_witness thy t =
    1.14    Witness (t, Goal.protect (Thm.assume (Thm.cterm_of thy t)));
    1.15  
    1.16 -fun prove_witness thy t tac =
    1.17 -  Witness (t, Goal.prove thy [] [] (Logic.protect t) (fn _ =>
    1.18 +fun prove_witness ctxt t tac =
    1.19 +  Witness (t, Goal.prove ctxt [] [] (Logic.protect t) (fn _ =>
    1.20      Tactic.rtac Drule.protectI 1 THEN tac));
    1.21  
    1.22  fun conclude_witness (Witness (_, th)) = Goal.norm_hhf (Goal.conclude th);