src/HOL/HOL.thy

--- a/src/HOL/HOL.thy	Mon Jun 14 10:38:28 2010 +0200
+++ b/src/HOL/HOL.thy	Mon Jun 14 10:38:29 2010 +0200
@@ -1800,8 +1800,8 @@
 setup {*
   Code_Preproc.map_pre (fn simpset =>
     simpset addsimprocs [Simplifier.simproc_i @{theory} "eq" [@{term "op ="}]
-      (fn thy => fn _ => fn t as Const (_, T) => case strip_type T
-        of ((T as Type _) :: _, _) => SOME @{thm equals_eq}
+      (fn thy => fn _ => fn Const (_, T) => case strip_type T
+        of (Type _ :: _, _) => SOME @{thm equals_eq}
          | _ => NONE)])
 *}