1.1 --- a/src/HOL/Tools/Function/mutual.ML	Thu Jul 16 23:12:12 2009 +0200
     1.2 +++ b/src/HOL/Tools/Function/mutual.ML	Fri Jul 17 21:32:58 2009 +0200
     1.3 @@ -100,7 +100,7 @@
     1.4          val (caTss, resultTs) = split_list (map curried_types fs)
     1.5          val argTs = map (foldr1 HOLogic.mk_prodT) caTss
     1.6  
     1.7 -        val dresultTs = distinct (Type.eq_type Vartab.empty) resultTs
     1.8 +        val dresultTs = distinct (op =) resultTs
     1.9          val n' = length dresultTs
    1.10  
    1.11          val RST = BalancedTree.make (uncurry SumTree.mk_sumT) dresultTs
    1.12 @@ -114,7 +114,7 @@
    1.13          fun define (fvar as (n, T)) caTs resultT i =
    1.14              let
    1.15                  val vars = map_index (fn (j,T) => Free ("x" ^ string_of_int j, T)) caTs (* FIXME: Bind xs properly *)
    1.16 -                val i' = find_index (fn Ta => Type.eq_type Vartab.empty (Ta, resultT)) dresultTs + 1 
    1.17 +                val i' = find_index (fn Ta => Ta = resultT) dresultTs + 1 
    1.18  
    1.19                  val f_exp = SumTree.mk_proj RST n' i' (Free fsum_var $ SumTree.mk_inj ST num i (foldr1 HOLogic.mk_prod vars))
    1.20                  val def = Term.abstract_over (Free fsum_var, fold_rev lambda vars f_exp)