# HG changeset patch
# User haftmann
# Date 1276504709 -7200
# Node ID 6cde0764bc0358c280de344c1090d049607592f5
# Parent  1cf6f134e7f209730d5caa6f4fb128430e01ffa8
dropped unused bindings

diff -r 1cf6f134e7f2 -r 6cde0764bc03 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)])
 *}