src/HOL/TLA/Memory/MemoryParameters.thy

--- a/src/HOL/TLA/Memory/MemoryParameters.thy	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/TLA/Memory/MemoryParameters.thy	Fri Jul 24 13:19:38 1998 +0200
@@ -9,7 +9,7 @@
     RPC-Memory example: Memory parameters
 *)
 
-MemoryParameters = Prod + Sum + Arith + RPCMemoryParams +
+MemoryParameters = Datatype + RPCMemoryParams +
 
 (* the memory operations. nb: data types must be defined in theories
    that do not include Intensional -- otherwise the induction rule