# HG changeset patch
# User wenzelm
# Date 1004459583 -3600
# Node ID 06658189cd5138c753aaf91786fec427c919209e
# Parent  324f69149895dc7c3531fe22a711bb0b1542abcf
tuned;

diff -r 324f69149895 -r 06658189cd51 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Oct 30 17:30:21 2001 +0100
+++ b/src/Pure/Isar/proof.ML	Tue Oct 30 17:33:03 2001 +0100
@@ -123,7 +123,7 @@
 datatype kind =
   Theorem of string * theory attribute list |    (*top-level theorem*)
   Show of context attribute list |               (*intermediate result, solving subgoal*)
-  Have of context attribute list ;               (*intermediate result*)
+  Have of context attribute list;                (*intermediate result*)
 
 val kind_name = fn Theorem (s, _) => s | Show _ => "show" | Have _ => "have";