# HG changeset patch
# User blanchet
# Date 1381308463 -7200
# Node ID 40366d99fa39b87413a82bf78705033e56c5227b
# Parent  957115f3dae4927880945de475c1adac86d95c9c
minor performance tuning

diff -r 957115f3dae4 -r 40366d99fa39 src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Wed Oct 09 09:53:18 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Wed Oct 09 10:47:43 2013 +0200
@@ -201,18 +201,22 @@
 
 fun patternT_ord p =
   case p of
-    (TVar _, TVar _) => EQUAL
+    (Type (s, ps), Type (t, qs)) =>
+    (case fast_string_ord (s, t) of
+      EQUAL => dict_ord patternT_ord (ps, qs)
+    | ord => ord)
+  | (TVar _, TVar _) => EQUAL
   | (TVar _, Type _) => LESS
   | (TVar _, TFree _) => LESS
   | (Type _, TVar _) => GREATER
   | (TFree _, TVar _) => GREATER
-  | (Type q1, Type q2) =>
-    prod_ord fast_string_ord (dict_ord patternT_ord) (q1, q2)
   | (Type _, TFree _) => LESS
   | (TFree _, Type _) => GREATER
   | (TFree (s, _), TFree (t, _)) => fast_string_ord (s, t)
-fun ptype_ord (PType p, PType q) =
-  prod_ord (dict_ord patternT_ord) int_ord (swap p, swap q)
+fun ptype_ord (PType (m, ps), PType (n, qs)) =
+  (case dict_ord patternT_ord (ps, qs) of
+    EQUAL => int_ord (m, n)
+  | ord => ord)
 
 structure PType_Tab = Table(type key = ptype val ord = ptype_ord)