1.1 --- a/src/Pure/Isar/skip_proof.ML	Wed Aug 02 22:26:40 2006 +0200
     1.2 +++ b/src/Pure/Isar/skip_proof.ML	Wed Aug 02 22:26:41 2006 +0200
     1.3 @@ -9,8 +9,8 @@
     1.4  sig
     1.5    val make_thm: theory -> term -> thm
     1.6    val cheat_tac: theory -> tactic
     1.7 -  val prove: ProofContext.context -> string list -> term list -> term ->
     1.8 -    ({prems: thm list, context: Context.proof} -> tactic) -> thm
     1.9 +  val prove: Proof.context -> string list -> term list -> term ->
    1.10 +    ({prems: thm list, context: Proof.context} -> tactic) -> thm
    1.11  end;
    1.12  
    1.13  structure SkipProof: SKIP_PROOF =