src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML

   fold (fn Obtain _ => Integer.add 1
          | Prove (_, _, _, By_Metis _) => Integer.add 1
          | Prove (_, _, _, Case_Split (cases, _)) =>
            Integer.add (fold (Integer.add o metis_steps_total) cases 1)
          | Prove (_, _, _, Subblock subproof) =>
-           Integer.add (metis_steps_total subproof)
+           Integer.add (metis_steps_total subproof + 1)
          | _ => I) proof 0
 
 end