diff -r 21423597a80d -r b8a53e3a0ee2 src/HOL/SET_Protocol/Public_SET.thy
--- a/src/HOL/SET_Protocol/Public_SET.thy	Tue Sep 28 12:47:55 2010 +0200
+++ b/src/HOL/SET_Protocol/Public_SET.thy	Tue Sep 28 12:47:55 2010 +0200
@@ -64,7 +64,11 @@
    RCA and CAs know their own respective keys;
    RCA (has already certified and therefore) knows all CAs public keys; 
    Spy knows all keys of all bad agents.*}
-primrec    
+
+overloading initState \<equiv> "initState"
+begin
+
+primrec initState where
 (*<*)
   initState_CA:
     "initState (CA i)  =
@@ -74,29 +78,31 @@
               Key (pubEK (CA i)), Key (pubSK (CA i)),
               Key (pubEK RCA), Key (pubSK RCA)})"
 
-  initState_Cardholder:
+| initState_Cardholder:
     "initState (Cardholder i)  =    
        {Key (priEK (Cardholder i)), Key (priSK (Cardholder i)),
         Key (pubEK (Cardholder i)), Key (pubSK (Cardholder i)),
         Key (pubEK RCA), Key (pubSK RCA)}"
 
-  initState_Merchant:
+| initState_Merchant:
     "initState (Merchant i)  =    
        {Key (priEK (Merchant i)), Key (priSK (Merchant i)),
         Key (pubEK (Merchant i)), Key (pubSK (Merchant i)),
         Key (pubEK RCA), Key (pubSK RCA)}"
 
-  initState_PG:
+| initState_PG:
     "initState (PG i)  = 
        {Key (priEK (PG i)), Key (priSK (PG i)),
         Key (pubEK (PG i)), Key (pubSK (PG i)),
         Key (pubEK RCA), Key (pubSK RCA)}"
 (*>*)
-  initState_Spy:
+| initState_Spy:
     "initState Spy = Key ` (invKey ` pubEK ` bad Un
                             invKey ` pubSK ` bad Un
                             range pubEK Un range pubSK)"
 
+end
+
 
 text{*Injective mapping from agents to PANs: an agent can have only one card*}