src/HOL/Tools/Lifting/lifting_term.ML

     fun generate (ty as Type (s, tys)) (table_ctxt as (table, ctxt)) =
       if null tys 
       then 
         let 
           val instantiated_id_quot_thm =
-            instantiate' [SOME (Thm.ctyp_of ctxt ty)] [] @{thm identity_quotient}
+            Thm.instantiate' [SOME (Thm.ctyp_of ctxt ty)] [] @{thm identity_quotient}
         in
           (instantiated_id_quot_thm, (table, ctxt)) 
         end
       else
         let