src/HOL/Tools/inductive_package.ML
changeset 16287 7a03b4b4df67
parent 16122 864fda4a4056
child 16364 dc9f7066d80a
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Sun Jun 05 23:07:24 2005 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Sun Jun 05 23:07:25 2005 +0200
     1.3 @@ -193,8 +193,7 @@
     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 -    val subst = fst o Type.freeze_thaw o
     1.8 -      (map_term_types (Envir.norm_type env))
     1.9 +    val subst = Type.freeze o map_term_types (Envir.norm_type env)
    1.10  
    1.11    in (map subst cs', map subst intr_ts')
    1.12    end) handle Type.TUNIFY =>