# HG changeset patch
# User blanchet
# Date 1282722148 -7200
# Node ID 69fa75354c5853f9753497b89ccdbe7e990b6192
# Parent  4fe1bb9e74346cbc0cb4098cbb8a18b3d7f6be92
simplify more code

diff -r 4fe1bb9e7434 -r 69fa75354c58 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Wed Aug 25 09:34:28 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Wed Aug 25 09:42:28 2010 +0200
@@ -164,26 +164,20 @@
 
 (**** Constant / Type Frequencies ****)
 
-(*A two-dimensional symbol table counts frequencies of constants. It's keyed first by
-  constant name and second by its list of type instantiations. For the latter, we need
-  a linear ordering on type const_typ list.*)
-
-local
-
-fun cons_nr CTVar = 0
-  | cons_nr (CType _) = 1;
+(* A two-dimensional symbol table counts frequencies of constants. It's keyed
+   first by constant name and second by its list of type instantiations. For the
+   latter, we need a linear ordering on "const_typ list". *)
 
-in
+fun const_typ_ord p =
+  case p of
+    (CTVar, CTVar) => EQUAL
+  | (CTVar, CType _) => LESS
+  | (CType _, CTVar) => GREATER
+  | (CType q1, CType q2) =>
+    prod_ord fast_string_ord (dict_ord const_typ_ord) (q1, q2)
 
-fun const_typ_ord TU =
-  case TU of
-    (CType (a, Ts), CType (b, Us)) =>
-      (case fast_string_ord(a,b) of EQUAL => dict_ord const_typ_ord (Ts,Us) | ord => ord)
-  | (T, U) => int_ord (cons_nr T, cons_nr U);
-
-end;
-
-structure CTtab = Table(type key = const_typ list val ord = dict_ord const_typ_ord);
+structure CTtab =
+  Table(type key = const_typ list val ord = dict_ord const_typ_ord)
 
 fun count_axiom_consts theory_relevant thy (_, th) =
   let