# HG changeset patch
# User wenzelm
# Date 1247859178 -7200
# Node ID 94b4a921c88dd25d3e841465ccbbb6bf014de594
# Parent  47122b809e3785a06d4091cc7c072351173d428d
compare types directly -- no need to invoke Type.eq_type with empty environment;

diff -r 47122b809e37 -r 94b4a921c88d src/HOL/Tools/Function/mutual.ML
--- a/src/HOL/Tools/Function/mutual.ML	Thu Jul 16 23:12:12 2009 +0200
+++ b/src/HOL/Tools/Function/mutual.ML	Fri Jul 17 21:32:58 2009 +0200
@@ -100,7 +100,7 @@
         val (caTss, resultTs) = split_list (map curried_types fs)
         val argTs = map (foldr1 HOLogic.mk_prodT) caTss
 
-        val dresultTs = distinct (Type.eq_type Vartab.empty) resultTs
+        val dresultTs = distinct (op =) resultTs
         val n' = length dresultTs
 
         val RST = BalancedTree.make (uncurry SumTree.mk_sumT) dresultTs
@@ -114,7 +114,7 @@
         fun define (fvar as (n, T)) caTs resultT i =
             let
                 val vars = map_index (fn (j,T) => Free ("x" ^ string_of_int j, T)) caTs (* FIXME: Bind xs properly *)
-                val i' = find_index (fn Ta => Type.eq_type Vartab.empty (Ta, resultT)) dresultTs + 1 
+                val i' = find_index (fn Ta => Ta = resultT) dresultTs + 1 
 
                 val f_exp = SumTree.mk_proj RST n' i' (Free fsum_var $ SumTree.mk_inj ST num i (foldr1 HOLogic.mk_prod vars))
                 val def = Term.abstract_over (Free fsum_var, fold_rev lambda vars f_exp)