diff -r cb3612cc41a3 -r fc075ae929e4 src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Sun Jan 30 20:48:50 2005 +0100
+++ b/src/HOL/Library/Word.thy	Tue Feb 01 18:01:57 2005 +0100
@@ -455,7 +455,7 @@
 	proof (rule n_div_2_cases [of n])
 	  assume [simp]: "n = 0"
 	  show ?thesis
-	    apply (subst nat_to_bv_helper.simps [of n])
+	    apply (simp only: nat_to_bv_helper.simps [of n])
 	    apply simp
 	    done
 	next
@@ -467,7 +467,7 @@
 	  have ind': "\<forall>l. nat_to_bv_helper (n div 2) l = nat_to_bv_helper (n div 2) [] @ l"
 	    by blast
 	  show ?thesis
-	    apply (subst nat_to_bv_helper.simps [of n])
+	    apply (simp only: nat_to_bv_helper.simps [of n])
 	    apply (cases "n=0")
 	    apply simp
 	    apply (simp only: if_False)
@@ -491,7 +491,7 @@
   assume [simp]: "0 < n"
   show ?thesis
     apply (subst nat_to_bv_def [of n])
-    apply (subst nat_to_bv_helper.simps [of n])
+    apply (simp only: nat_to_bv_helper.simps [of n])
     apply (subst unfold_nat_to_bv_helper)
     using prems
     apply simp
@@ -545,7 +545,7 @@
       by simp
     show ?thesis
       apply (subst nat_to_bv_def)
-      apply (subst nat_to_bv_helper.simps [of n])
+      apply (simp only: nat_to_bv_helper.simps [of n])
       apply (simp only: n0' if_False)
       apply (subst unfold_nat_to_bv_helper)
       apply (subst bv_to_nat_dist_append)
@@ -2425,7 +2425,7 @@
 
   from ki ij jl lw
   show ?thesis
-    apply (subst bv_sliceI [where ?j = i and ?i = j and ?w = w and ?w1.0 = "w1 @ w2" and ?w2.0 = w3 and ?w3.0 = "w4 @ w5"])
+    apply (simplesubst bv_sliceI [where ?j = i and ?i = j and ?w = w and ?w1.0 = "w1 @ w2" and ?w2.0 = w3 and ?w3.0 = "w4 @ w5"])
     apply simp_all
     apply (rule w_def)
     apply (simp add: w_defs min_def)
@@ -2566,7 +2566,7 @@
       apply (subst indq [symmetric])
       apply (subst indq [symmetric])
       apply auto
-      apply (subst nat_to_bv_helper.simps [of "2 * qq + 1"])
+      apply (simp only: nat_to_bv_helper.simps [of "2 * qq + 1"])
       apply simp
       apply safe
       apply (subgoal_tac "2 * qq + 1 ~= 2 * q")
@@ -2575,7 +2575,7 @@
       apply (subgoal_tac "(2 * qq + 1) div 2 = qq")
       apply simp
       apply (subst zdiv_zadd1_eq,simp)
-      apply (subst nat_to_bv_helper.simps [of "2 * qq"])
+      apply (simp only: nat_to_bv_helper.simps [of "2 * qq"])
       apply simp
       done
   qed