src/HOL/Tools/inductive_package.ML
changeset 15794 5de27a5fc5ed
parent 15705 b5edb9dcec9a
child 16122 864fda4a4056
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Apr 21 18:56:03 2005 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Apr 21 18:57:18 2005 +0200
     1.3 @@ -193,10 +193,8 @@
     1.4            (env, (replicate (length consts) cT) ~~ consts)
     1.5        end;
     1.6      val (env, _) = Library.foldl unify ((Vartab.empty, i'), rec_consts);
     1.7 -    fun typ_subst_TVars_2 env T = let val T' = typ_subst_TVars_Vartab env T
     1.8 -      in if T = T' then T else typ_subst_TVars_2 env T' end;
     1.9      val subst = fst o Type.freeze_thaw o
    1.10 -      (map_term_types (typ_subst_TVars_2 env))
    1.11 +      (map_term_types (Envir.norm_type env))
    1.12  
    1.13    in (map subst cs', map subst intr_ts')
    1.14    end) handle Type.TUNIFY =>