diff -r ba465fcd0267 -r 8c6226d88ced src/HOL/HOLCF/IOA/ex/TrivEx.thy
--- a/src/HOL/HOLCF/IOA/ex/TrivEx.thy	Wed Dec 30 22:05:00 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ex/TrivEx.thy	Wed Dec 30 22:09:44 2015 +0100
@@ -45,7 +45,7 @@
   "h_abs n = (n~=0)"
 
 axiomatization where
-  MC_result: "validIOA A_ioa (\<diamond>\<box><%(b,a,c). b>)"
+  MC_result: "validIOA A_ioa (\<diamond>\<box>\<langle>%(b,a,c). b\<rangle>)"
 
 lemma h_abs_is_abstraction:
   "is_abstraction h_abs C_ioa A_ioa"
@@ -61,7 +61,7 @@
 apply (simp add: h_abs_def)
 done
 
-lemma TrivEx_abstraction: "validIOA C_ioa (\<diamond>\<box><%(n,a,m). n~=0>)"
+lemma TrivEx_abstraction: "validIOA C_ioa (\<diamond>\<box>\<langle>%(n,a,m). n~=0\<rangle>)"
 apply (rule AbsRuleT1)
 apply (rule h_abs_is_abstraction)
 apply (rule MC_result)