src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML

           |> enrich_context_with_local_facts canonical_isar_proof
           |> silence_reconstructors debug
 
         val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty
 
-        fun reset_preplay_outcomes (step as Prove (_, _, l, _, _, (_, meths))) =
+        fun init_preplay_outcomes (step as Prove (_, _, l, _, _, (_, meths))) =
             set_preplay_outcomes_of_isar_step preplay_data l (map (fn meth => (meth,
                 Lazy.lazy (fn () => preplay_isar_step preplay_ctxt preplay_timeout meth step)))
               meths)
-          | reset_preplay_outcomes _ = ()
-
-        val _ = fold_isar_steps (K o reset_preplay_outcomes)
+          | init_preplay_outcomes _ = ()
+
+        val _ = fold_isar_steps (K o init_preplay_outcomes)
           (steps_of_isar_proof canonical_isar_proof) ()
 
         fun str_of_preplay_outcome outcome =
           if Lazy.is_finished outcome then string_of_play_outcome (Lazy.force outcome) else "?"