diff -r 3b2c770f6631 -r 521508e85c0d src/HOL/IMP/Star.thy
--- a/src/HOL/IMP/Star.thy	Tue Oct 25 12:00:52 2011 +0200
+++ b/src/HOL/IMP/Star.thy	Tue Oct 25 15:59:15 2011 +0200
@@ -7,6 +7,8 @@
 refl:  "star r x x" |
 step:  "r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
 
+hide_fact (open) refl step  --"names too generic"
+
 lemma star_trans:
   "star r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
 proof(induction rule: star.induct)
@@ -19,8 +21,8 @@
 
 declare star.refl[simp,intro]
 
-lemma step1[simp, intro]: "r x y \<Longrightarrow> star r x y"
-by(metis refl step)
+lemma star_step1[simp, intro]: "r x y \<Longrightarrow> star r x y"
+by(metis star.refl star.step)
 
 code_pred star .