author | haftmann |
Mon, 14 Jun 2010 10:38:29 +0200 | |
changeset 37421 | 6cde0764bc03 |
parent 37420 | 1cf6f134e7f2 |
child 37422 | 6d19e4e6ebf5 |
src/HOL/HOL.thy | file | annotate | diff | comparison | revisions |
--- 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)]) *}