diff -r e96292f32c3c -r 38b73f7940af src/HOL/Auth/Public.thy
--- a/src/HOL/Auth/Public.thy	Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/Public.thy	Mon Dec 28 23:13:33 2015 +0100
@@ -239,13 +239,13 @@
 apply (auto dest!: parts_cut simp add: used_Nil) 
 done
 
-lemma MPair_used_D: "{|X,Y|} \<in> used H ==> X \<in> used H & Y \<in> used H"
+lemma MPair_used_D: "\<lbrace>X,Y\<rbrace> \<in> used H ==> X \<in> used H & Y \<in> used H"
 by (drule used_parts_subset_parts, simp, blast)
 
 text\<open>There was a similar theorem in Event.thy, so perhaps this one can
   be moved up if proved directly by induction.\<close>
 lemma MPair_used [elim!]:
-     "[| {|X,Y|} \<in> used H;
+     "[| \<lbrace>X,Y\<rbrace> \<in> used H;
          [| X \<in> used H; Y \<in> used H |] ==> P |] 
       ==> P"
 by (blast dest: MPair_used_D)