# HG changeset patch
# User wenzelm
# Date 1291211767 -3600
# Node ID 6c7d2a8761ed61cb09ad9b468cfb98f40519dd14
# Parent  82baff065334ba9f52e6bf34a722df520b3bdfb1
simplified HOL.eq simproc matching;

diff -r 82baff065334 -r 6c7d2a8761ed src/HOL/HOL.thy
--- 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)])
 *}