src/HOL/Auth/Message.thy

--- a/src/HOL/Auth/Message.thy	Tue Jun 30 20:50:34 1998 +0200
+++ b/src/HOL/Auth/Message.thy	Tue Jun 30 20:51:15 1998 +0200
@@ -7,7 +7,7 @@
 Inductive relations "parts", "analz" and "synth"
 *)
 
-Message = Arith +
+Message = Arith + Inductive +
 
 (*Is there a difference between a nonce and arbitrary numerical data?
   Do we need a type of nonces?*)