# HG changeset patch
# User wenzelm
# Date 1124356669 -7200
# Node ID 8638a0a0a668f01ba945cc1d5ab6ca380fe4486a
# Parent  3b67c1809e1c3033bd78140232be1d3d4c88becb
accomodate interface Proof vs. Method;

diff -r 3b67c1809e1c -r 8638a0a0a668 src/Pure/Isar/skip_proof.ML
--- a/src/Pure/Isar/skip_proof.ML	Thu Aug 18 11:17:48 2005 +0200
+++ b/src/Pure/Isar/skip_proof.ML	Thu Aug 18 11:17:49 2005 +0200
@@ -13,8 +13,8 @@
   val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
   val local_skip_proof: (Proof.context -> string * (string * thm list) list -> unit) *
     (Proof.context -> thm -> unit) -> bool -> Proof.state -> Proof.state Seq.seq
-  val global_skip_proof:
-    bool -> Proof.state -> theory * ((string * string) * (string * thm list) list)
+  val global_skip_proof: bool -> Proof.state ->
+    (theory * Proof.context) * ((string * string) * (string * thm list) list)
 end;
 
 structure SkipProof: SKIP_PROOF =
@@ -56,8 +56,8 @@
 fun cheating int ctxt = Method.METHOD (K (setmp quick_and_dirty (int orelse ! quick_and_dirty)
     (cheat_tac (ProofContext.theory_of ctxt))));
 
-fun local_skip_proof x int = Method.local_terminal_proof (Method.Basic (cheating int), NONE) x;
-fun global_skip_proof int = Method.global_terminal_proof (Method.Basic (cheating int), NONE);
+fun local_skip_proof x int = Proof.local_terminal_proof (Method.Basic (cheating int), NONE) x;
+fun global_skip_proof int = Proof.global_terminal_proof (Method.Basic (cheating int), NONE);
 
 end;