src/HOL/Auth/Event.ML

--- a/src/HOL/Auth/Event.ML	Thu Jul 02 17:27:35 1998 +0200
+++ b/src/HOL/Auth/Event.ML	Thu Jul 02 17:48:11 1998 +0200
@@ -22,8 +22,7 @@
 	  read_instantiate_sg (sign_of thy) [("H", "spies evs")]);
 
 
-Goal
-    "P(event_case sf nf ev) = \
+Goal "P(event_case sf nf ev) = \
 \      ((ALL A B X. ev = Says A B X --> P(sf A B X)) & \
 \       (ALL A X. ev = Notes A X --> P(nf A X)))";
 by (induct_tac "ev" 1);