src/HOL/Tools/function_package/mutual.ML

 	val plain_eq = sum_psimp
                          |> fold (implies_elim_swp o assume) conds
 
 	val x = Free ("x", RST)
 
-	val f_def_inst = instantiate' [] (map (SOME o cterm_of thy) args) (freezeT f_def) (* FIXME: freezeT *)
+	val f_def_inst = instantiate' [] (map (SOME o cterm_of thy) args) (Thm.freezeT f_def) (* FIXME: freezeT *)
     in
 	reflexive (cterm_of thy (lambda x (SumTools.mk_proj streeR pthR x)))  (*  PR(x) == PR(x) *)
 		  |> (fn it => combination it (plain_eq RS eq_reflection))
 		  |> beta_norm_eq (*  PR(S(I(as))) == PR(IR(...)) *)
 		  |> transitive f_def_inst (*  f ... == PR(IR(...)) *)