src/HOL/Tools/function_package/mutual.ML

       val xs = map_index (fn (i,T) => cterm_of thy (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *)
     in
       fold (fn x => fn thm => combination thm (reflexive x)) xs thm
            |> Conv.fconv_rule (Thm.beta_conversion true)
            |> fold_rev forall_intr xs
-           |> forall_elim_vars 0
+           |> Thm.forall_elim_vars 0
     end
 
 
 fun mutual_induct_rules lthy induct all_f_defs (Mutual {n, ST, RST, parts, ...}) =
     let