src/HOL/Import/import_rule.ML

        Drule.instantiate'
           [SOME nty, SOME oty]
           [SOME rept, SOME abst, SOME cP, SOME (cterm_of thy' (Free ("a", aty))),
              SOME (cterm_of thy' (Free ("r", typ_of ctT)))]
           @{thm typedef_hol2hollight}
-    val th4 = meta_mp typedef_th (#type_definition (#2 typedef_info))
+    val th4 = typedef_th OF [#type_definition (#2 typedef_info)]
   in
     (th4, thy')
   end
 
 fun mtydef name thy =