# HG changeset patch
# User nipkow
# Date 1512547887 -3600
# Node ID fa1173288322a146f659d513bf5e752fc25a6d6a
# Parent  94fca35f80abd9d70ecbd03f6ed38c252891565c
tuned

diff -r 94fca35f80ab -r fa1173288322 src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Tue Dec 05 16:54:37 2017 +0100
+++ b/src/HOL/Word/Bit_Representation.thy	Wed Dec 06 09:11:27 2017 +0100
@@ -139,14 +139,8 @@
 lemma bin_ex_rl: "\<exists>w b. w BIT b = bin"
   by (metis bin_rl_simp)
 
-lemma bin_exhaust:
-  assumes that: "\<And>x b. bin = x BIT b \<Longrightarrow> Q"
-  shows "Q"
-  apply (insert bin_ex_rl [of bin])
-  apply (erule exE)+
-  apply (rule that)
-  apply force
-  done
+lemma bin_exhaust: "(\<And>x b. bin = x BIT b \<Longrightarrow> Q) \<Longrightarrow> Q"
+by (metis bin_ex_rl)
 
 primrec bin_nth
   where