1.1 --- a/src/Pure/Isar/element.ML	Fri Oct 26 16:12:58 2007 +0200
     1.2 +++ b/src/Pure/Isar/element.ML	Fri Oct 26 17:18:32 2007 +0200
     1.3 @@ -291,10 +291,11 @@
     1.4    Witness (t, Goal.protect (Thm.assume (Thm.cterm_of thy t)));
     1.5  
     1.6  fun prove_witness ctxt t tac =
     1.7 -  Witness (t, Goal.prove ctxt [] [] (Logic.protect t) (fn _ =>
     1.8 -    Tactic.rtac Drule.protectI 1 THEN tac));
     1.9 +  Witness (t, Goal.close_result (Goal.prove ctxt [] [] (Logic.protect t) (fn _ =>
    1.10 +    Tactic.rtac Drule.protectI 1 THEN tac)));
    1.11  
    1.12 -fun conclude_witness (Witness (_, th)) = MetaSimplifier.norm_hhf_protect (Goal.conclude th);
    1.13 +fun conclude_witness (Witness (_, th)) =
    1.14 +  Goal.close_result (MetaSimplifier.norm_hhf_protect (Goal.conclude th));
    1.15  
    1.16  val mark_witness = Logic.protect;
    1.17