1.1 --- a/src/HOL/Tools/record.ML	Fri Dec 02 14:54:25 2011 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Fri Dec 02 15:23:27 2011 +0100
     1.3 @@ -1495,7 +1495,7 @@
     1.4    let
     1.5      val ctxt' = fold (Variable.declare_typ o TFree) env ctxt;
     1.6      val T = Syntax.read_typ ctxt' raw_T;
     1.7 -    val env' = Misc_Legacy.add_typ_tfrees (T, env);
     1.8 +    val env' = Term.add_tfreesT T env;
     1.9    in (T, env') end;
    1.10  
    1.11  fun cert_typ ctxt raw_T env =
    1.12 @@ -1503,7 +1503,7 @@
    1.13      val thy = Proof_Context.theory_of ctxt;
    1.14      val T = Type.no_tvars (Sign.certify_typ thy raw_T)
    1.15        handle TYPE (msg, _, _) => error msg;
    1.16 -    val env' = Misc_Legacy.add_typ_tfrees (T, env);
    1.17 +    val env' = Term.add_tfreesT T env;
    1.18    in (T, env') end;
    1.19  
    1.20