diff -r bdc835d934b7 -r b4bf82ed0ad5 src/HOL/Word/Bits.thy
--- a/src/HOL/Word/Bits.thy	Mon Apr 22 09:33:55 2019 +0000
+++ b/src/HOL/Word/Bits.thy	Mon Apr 22 09:33:55 2019 +0000
@@ -1,5 +1,5 @@
 (*  Title:      HOL/Word/Bits.thy
-    Author:     Author: Brian Huffman, PSU and Gerwin Klein, NICTA
+    Author:     Brian Huffman, PSU and Gerwin Klein, NICTA
 *)
 
 section \<open>Syntactic type classes for bit operations\<close>
@@ -19,7 +19,6 @@
     and lsb :: "'a \<Rightarrow> bool"
     and msb :: "'a \<Rightarrow> bool"
     and set_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> 'a"
-    and set_bits :: "(nat \<Rightarrow> bool) \<Rightarrow> 'a"  (binder "BITS " 10)
 
 text \<open>
   We want the bitwise operations to bind slightly weaker