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