Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML
changeset 51132 f8dc1c94ef8b
parent 51128 0021ea861129
child 51147 020a6812a204 
--- 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
isabelle