| changeset 23520 | 483fe92f00c1 |
| parent 23514 | 25e69e56355d |
| child 23523 | d52108dd4b6c |
--- a/src/HOL/Tools/Qelim/cooper.ML Fri Jun 29 18:21:25 2007 +0200 +++ b/src/HOL/Tools/Qelim/cooper.ML Fri Jun 29 21:23:05 2007 +0200 @@ -13,7 +13,7 @@ struct open Conv; open Normalizer; -structure Integertab = TableFun(type key = integer val ord = Integer.cmp); +structure Integertab = TableFun(type key = Integer.int val ord = Integer.ord); exception COOPER of string * exn; val simp_thms_conv = Simplifier.rewrite (HOL_basic_ss addsimps simp_thms);