# HG changeset patch
# User wenzelm
# Date 931811336 -7200
# Node ID 26d43e26ea61af179de07aa7cd5c21dba635fef0
# Parent  7f28cd9cfe72dd14c29d389bada59d568d1f970b
local qed; print rule;

diff -r 7f28cd9cfe72 -r 26d43e26ea61 src/Pure/Isar/skip_proof.ML
--- a/src/Pure/Isar/skip_proof.ML	Mon Jul 12 22:28:38 1999 +0200
+++ b/src/Pure/Isar/skip_proof.ML	Mon Jul 12 22:28:56 1999 +0200
@@ -7,7 +7,7 @@
 
 signature SKIP_PROOF =
 sig
-  val local_skip_proof: ({kind: string, name: string, thm: thm} -> unit)
+  val local_skip_proof: ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit)
     -> Proof.state -> Proof.state Seq.seq
   val global_skip_proof: Proof.state -> theory * {kind: string, name: string, thm: thm}
   val setup: (theory -> theory) list