src/HOL/Nominal/nominal_inductive.ML

         ("fs_" ^ Long_Name.base_name (fst (dest_Type T)))) atomTs));
     val (fs_ctxt_tyname, _) = Name.variant "'n" (Variable.names_of ctxt');
     val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt';
     val fsT = TFree (fs_ctxt_tyname, ind_sort);
 
-    val inductive_forall_def' = Drule.instantiate'
+    val inductive_forall_def' = Thm.instantiate'
       [SOME (Thm.global_ctyp_of thy fsT)] [] inductive_forall_def;
 
     fun lift_pred' t (Free (s, T)) ts =
       list_comb (Free (s, fsT --> T), t :: ts);
     val lift_pred = lift_pred' (Bound 0);

                     in
                       (map (fn th =>
                          let
                            val (cf, ct) =
                              Thm.dest_comb (Thm.dest_arg (Thm.cprop_of th));
-                           val arg_cong' = Drule.instantiate'
+                           val arg_cong' = Thm.instantiate'
                              [SOME (Thm.ctyp_of_cterm ct)]
                              [NONE, SOME ct, SOME cf] (arg_cong RS iffD2);
                            val inst = Thm.first_order_match (ct,
                              Thm.dest_arg (Thm.dest_arg (Thm.cprop_of th')))
                          in [th', th] MRS Thm.instantiate inst arg_cong'