src/HOL/Auth/TLS.thy

          "%((x,y,z), r). prod_encode(role_case 0 1 r, 
                            prod_encode(x, prod_encode(y,z)))"])
    apply (simp add: inj_on_def prod_encode_eq split: role.split) 
    done
 
-axioms
+axiomatization where
   --{*sessionK makes symmetric keys*}
-  isSym_sessionK: "sessionK nonces \<in> symKeys"
+  isSym_sessionK: "sessionK nonces \<in> symKeys" and
 
   --{*sessionK never clashes with a long-term symmetric key  
      (they don't exist in TLS anyway)*}
   sessionK_neq_shrK [iff]: "sessionK nonces \<noteq> shrK A"