src/HOL/Tools/old_primrec.ML
changeset 33832 cff42395c246
parent 33368 b1cf34f1855c
child 33955 fff6f11b1f09
     1.1 --- a/src/HOL/Tools/old_primrec.ML	Sat Nov 21 14:03:36 2009 +0100
     1.2 +++ b/src/HOL/Tools/old_primrec.ML	Sat Nov 21 15:49:29 2009 +0100
     1.3 @@ -45,7 +45,7 @@
     1.4        let val consts = map snd (filter (fn (c, _) => c = cname) intr_consts)
     1.5        in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end;
     1.6      val (env, _) = fold unify rec_consts (Vartab.empty, i');
     1.7 -    val subst = Type.freeze o map_types (Envir.norm_type env)
     1.8 +    val subst = Type.legacy_freeze o map_types (Envir.norm_type env)
     1.9  
    1.10    in (map subst cs', map subst intr_ts')
    1.11    end) handle Type.TUNIFY =>