--- a/src/Pure/Isar/skip_proof.ML Thu Apr 17 22:22:19 2008 +0200
+++ b/src/Pure/Isar/skip_proof.ML Thu Apr 17 22:22:21 2008 +0200
@@ -12,7 +12,7 @@
val prove: Proof.context -> string list -> term list -> term ->
({prems: thm list, context: Proof.context} -> tactic) -> thm
val prove_global: theory -> string list -> term list -> term ->
- (thm list -> tactic) -> thm
+ ({prems: thm list, context: Proof.context} -> tactic) -> thm
end;
structure SkipProof: SKIP_PROOF =
@@ -45,6 +45,6 @@
else tac args st);
fun prove_global thy xs asms prop tac =
- Drule.standard (prove (ProofContext.init thy) xs asms prop (fn {prems, ...} => tac prems));
+ Drule.standard (prove (ProofContext.init thy) xs asms prop tac);
end;