src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML

                 if is_referenced_in_step (the (label_of_isar_step lem)) step then
                   insert_lemma_in_step lem step @ steps
                 else
                   step :: insert_lemma_in_steps lem steps
             and insert_lemma_in_proof lem (proof as Proof {steps, ...}) =
-                isar_proof_with_steps proof (insert_lemma_in_steps lem steps)
+              isar_proof_with_steps proof (insert_lemma_in_steps lem steps)
 
             val rule_of_clause_id = fst o the o Symtab.lookup steps o fst
 
             val finish_off = close_form #> rename_bound_vars