author | wenzelm |
Sat, 08 May 2010 22:29:44 +0200 | |
changeset 36771 | 3e08b6789e66 |
parent 36762 | 40837a7b32a7 |
child 36772 | ef97c5006840 |
child 36774 | 9e444b09fbef |
--- a/src/HOL/Tools/semiring_normalizer.ML Sat May 08 21:25:25 2010 +0200 +++ b/src/HOL/Tools/semiring_normalizer.ML Sat May 08 22:29:44 2010 +0200 @@ -57,7 +57,7 @@ type T = (thm * entry) list; val empty = []; val extend = I; - val merge = AList.merge Thm.eq_thm (K true); + fun merge data = AList.merge Thm.eq_thm (K true) data; ); val get = Data.get o Context.Proof;