src/HOL/Tools/inductive_package.ML

 fun prove_intrs coind mono fp_def intr_ts con_defs rec_sets_defs thy =
   let
     val _ = message "  Proving the introduction rules ...";
 
     val unfold = standard (mono RS (fp_def RS
-      (if coind then def_gfp_Tarski else def_lfp_Tarski)));
+      (if coind then def_gfp_unfold else def_lfp_unfold)));
 
     fun select_disj 1 1 = []
       | select_disj _ 1 = [rtac disjI1]
       | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));