diff -r fea589c8583e -r 6da283e4497b src/HOL/IMP/Star.thy
--- a/src/HOL/IMP/Star.thy	Mon Nov 12 14:46:42 2012 +0100
+++ b/src/HOL/IMP/Star.thy	Mon Nov 12 18:42:49 2012 +0100
@@ -17,7 +17,8 @@
   case step thus ?case by (metis star.step)
 qed
 
-lemmas star_induct = star.induct[of "r:: 'a*'b \<Rightarrow> 'a*'b \<Rightarrow> bool", split_format(complete)]
+lemmas star_induct =
+  star.induct[of "r:: 'a*'b \<Rightarrow> 'a*'b \<Rightarrow> bool", split_format(complete)]
 
 declare star.refl[simp,intro]