src/HOL/Auth/Message.thy

--- a/src/HOL/Auth/Message.thy	Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/Auth/Message.thy	Fri Jul 24 13:03:20 1998 +0200
@@ -7,7 +7,7 @@
 Inductive relations "parts", "analz" and "synth"
 *)
 
-Message = Arith + Inductive +
+Message = Datatype +
 
 (*Is there a difference between a nonce and arbitrary numerical data?
   Do we need a type of nonces?*)