simplified HOL.eq simproc matching;

--- a/src/HOL/HOL.thy	Wed Dec 01 13:37:31 2010 +0100
+++ b/src/HOL/HOL.thy	Wed Dec 01 14:56:07 2010 +0100
@@ -1796,9 +1796,8 @@
 setup {*
   Code_Preproc.map_pre (fn simpset =>
     simpset addsimprocs [Simplifier.simproc_global_i @{theory} "equal" [@{term HOL.eq}]
-      (fn thy => fn _ => fn Const (_, T) => case strip_type T
-        of (Type _ :: _, _) => SOME @{thm eq_equal}
-         | _ => NONE)])
+      (fn thy => fn _ =>
+        fn Const (_, Type ("fun", [Type _, _])) => SOME @{thm eq_equal} | _ => NONE)])
 *}