src/Pure/Isar/skip_proof.ML
changeset 20289 ba7a7c56bed5
parent 20248 7916ce5bb069
child 24502 8d5326f0098b
--- 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 =