# HG changeset patch
# User smolkas
# Date 1360882486 -3600
# Node ID f8dc1c94ef8bf34b3774b5994276d7de3b5dc2ce
# Parent  7de262be1e95c038e2749d80ea708da0c158bb91
fixed metis_steps_total - was off by one

diff -r 7de262be1e95 -r f8dc1c94ef8b src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Thu Feb 14 22:49:22 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Thu Feb 14 23:54:46 2013 +0100
@@ -60,7 +60,7 @@
          | 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