# HG changeset patch
# User blanchet
# Date 1391551878 -3600
# Node ID 3c7f3122ccdcf407315727a69c6420ff9488aa85
# Parent  cc627ced387460e949adab8c6fcf129d8e730db0
do a second phase of proof compression after minimization

diff -r cc627ced3874 -r 3c7f3122ccdc src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Feb 04 23:11:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Feb 04 23:11:18 2014 +0100
@@ -322,6 +322,9 @@
                (keep_fastest_method_of_isar_step (!preplay_data)
                 #> minimize ? minimize_isar_step_dependencies ctxt preplay_data)
           |> tap (trace_isar_proof "Minimized")
+          |> minimize
+               ? (compress_isar_proof ctxt compress_isar preplay_data
+                  #> tap (trace_isar_proof "Compressed again"))
           |> `(preplay_outcome_of_isar_proof (!preplay_data))
           ||> (comment_isar_proof comment_of
                #> chain_isar_proof