diff -r e5b698bca555 -r 09f65e860bdb src/HOL/SizeChange/Correctness.thy
--- a/src/HOL/SizeChange/Correctness.thy	Thu Jul 09 23:05:59 2009 +0200
+++ b/src/HOL/SizeChange/Correctness.thy	Thu Jul 09 23:05:59 2009 +0200
@@ -250,7 +250,7 @@
 
     have "tcl A = A * star A"
       unfolding tcl_def
-      by (simp add: star_commute[of A A A, simplified])
+      by (simp add: star_simulation[of A A A, simplified])
 
     with edge
     have "has_edge (A * star A) x G y" by simp
@@ -272,7 +272,7 @@
     have "has_edge (star A * A) x G y" by (simp add:tcl_def)
     then obtain H H' z
       where AH': "has_edge A z H' y" and G: "G = H * H'"
-      by (auto simp:in_grcomp)
+      by (auto simp:in_grcomp simp del: star_slide2)
     from B
     obtain m' e' where "has_edge H' m' e' n"
       by (auto simp:G in_grcomp)