src/Pure/Isar/rule_insts.ML

         if is_tvar xi then
           T.assign (SOME (T.Typ (the (AList.lookup (op =) type_insts xi)))) arg
         else
           T.assign (SOME (T.Term (the (AList.lookup (op =) term_insts xi)))) arg);
   in
-    Drule.instantiate insts thm |> RuleCases.save thm
+    Drule.instantiate insts thm |> Rule_Cases.save thm
   end;
 
 fun read_instantiate_mixed' ctxt (args, concl_args) thm =
   let
     fun zip_vars _ [] = []