diff -r 8cba509ace9c -r 1f2788fb0b8b src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy	Wed Dec 30 21:52:00 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy	Wed Dec 30 21:56:12 2015 +0100
@@ -56,7 +56,7 @@
 apply simp
 done
 
-lemma corresp_ex_simC_cons: "(corresp_ex_simC A R$((a,t)>>xs)) s =
+lemma corresp_ex_simC_cons: "(corresp_ex_simC A R$((a,t)\<leadsto>xs)) s =
            (let T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t'
             in
              (@cex. move A cex s a T')
@@ -138,7 +138,7 @@
    "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>
     let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in
       mk_trace A$((@x. move A x s' a T')) =
-        (if a:ext A then a>>nil else nil)"
+        (if a:ext A then a\<leadsto>nil else nil)"
 apply (cut_tac move_is_move_sim)
 defer
 apply assumption+