diff -r ca45d6126c8a -r fe5f5510aef4 src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Fri Oct 16 08:48:05 1998 +0200
+++ b/src/HOL/Auth/Message.thy	Fri Oct 16 12:20:41 1998 +0200
@@ -7,10 +7,7 @@
 Inductive relations "parts", "analz" and "synth"
 *)
 
-Message = Datatype +
-
-(*Is there a difference between a nonce and arbitrary numerical data?
-  Do we need a type of nonces?*)
+Message = Main +
 
 types 
   key = nat