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_reconstruct.ML
changeset 50269 20a01c3e8072
parent 50267 1da2e67242d6
child 50271 2be84eaf7ebb 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Nov 28 12:25:43 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Nov 28 12:25:43 2012 +0100
@@ -702,7 +702,7 @@
           |>> kill_useless_labels_in_proof
           |>> relabel_proof
           |>> not (null params) ? cons (Fix params)
-        val num_steps = metis_steps_recursive isar_proof
+        val num_steps = metis_steps_total isar_proof
         val isar_text =
           string_for_proof ctxt type_enc lam_trans subgoal subgoal_count
                            isar_proof
isabelle