src/HOL/Tools/inductive_realizer.ML

         val rlz = Extraction.realizes_of thy (vs @ Ps) r (prop_of elim);
         val rlz' = attach_typeS (strip_all (Logic.unvarify_global rlz));
         val rews = map mk_meta_eq case_thms;
         val thm = Goal.prove_global thy []
           (Logic.strip_imp_prems rlz') (Logic.strip_imp_concl rlz') (fn {prems, ...} => EVERY
-          [cut_facts_tac [hd prems] 1,
+          [cut_tac (hd prems) 1,
            etac elimR 1,
            ALLGOALS (asm_simp_tac HOL_basic_ss),
            rewrite_goals_tac rews,
            REPEAT ((resolve_tac prems THEN_ALL_NEW (Object_Logic.atomize_prems_tac THEN'
              DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);