# HG changeset patch
# User wenzelm
# Date 1005511064 -3600
# Node ID a57873aec3bff495b3ec6fa9a60ddb925beb7209
# Parent  64e69a8a945f6300eadf302c08dd312ed464be76
adapted to multiple results;

diff -r 64e69a8a945f -r a57873aec3bf src/Pure/Isar/skip_proof.ML
--- a/src/Pure/Isar/skip_proof.ML	Sun Nov 11 21:37:20 2001 +0100
+++ b/src/Pure/Isar/skip_proof.ML	Sun Nov 11 21:37:44 2001 +0100
@@ -12,9 +12,9 @@
   val make_thm: theory -> term -> thm
   val cheat_tac: theory -> tactic
   val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
-  val local_skip_proof: (Proof.context -> {kind: string, name: string, thm: thm} -> unit) *
+  val local_skip_proof: (Proof.context -> string * (string * thm list) list -> unit) *
     (Proof.context -> thm -> unit) -> Proof.state -> Proof.state Seq.seq
-  val global_skip_proof: Proof.state -> theory * {kind: string, name: string, thm: thm}
+  val global_skip_proof: Proof.state -> theory * (string * (string * thm list) list)
   val setup: (theory -> theory) list
 end;