# HG changeset patch
# User nipkow
# Date 1319551155 -7200
# Node ID 521508e85c0dfe81278df19a27ffcf1c31dbcb32
# Parent  3b2c770f663140cf188f54bff22e34366edd15d2
tuned names to avoid shadowing

diff -r 3b2c770f6631 -r 521508e85c0d src/HOL/IMP/Small_Step.thy
--- a/src/HOL/IMP/Small_Step.thy	Tue Oct 25 12:00:52 2011 +0200
+++ b/src/HOL/IMP/Small_Step.thy	Tue Oct 25 15:59:15 2011 +0200
@@ -114,7 +114,7 @@
   let ?if = "IF b THEN c; WHILE b DO c ELSE SKIP"
   have "(WHILE b DO c,s) \<rightarrow> (?if, s)" by blast
   moreover have "(?if,s) \<rightarrow> (SKIP, s)" by (simp add: b)
-  ultimately show "(WHILE b DO c,s) \<rightarrow>* (SKIP,s)" by (metis refl step)
+  ultimately show "(WHILE b DO c,s) \<rightarrow>* (SKIP,s)" by(metis star.refl star.step)
 next
   fix b c s s' t
   let ?w  = "WHILE b DO c"
@@ -137,16 +137,16 @@
 next
   case Semi thus ?case by (blast intro: semi_comp)
 next
-  case IfTrue thus ?case by (blast intro: step)
+  case IfTrue thus ?case by (blast intro: star.step)
 next
-  case IfFalse thus ?case by (blast intro: step)
+  case IfFalse thus ?case by (blast intro: star.step)
 next
   case WhileFalse thus ?case
-    by (metis step step1 small_step.IfFalse small_step.While)
+    by (metis star.step star_step1 small_step.IfFalse small_step.While)
 next
   case WhileTrue
   thus ?case
-    by(metis While semi_comp small_step.IfTrue step[of small_step])
+    by(metis While semi_comp small_step.IfTrue star.step[of small_step])
 qed
 
 lemma small1_big_continue:
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 .