tuned;

--- 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";