# HG changeset patch
# User smolkas
# Date 1361717347 -3600
# Node ID 61bc5a3bef09f63a96329cd48370d1401cfa9b4e
# Parent  1491459df1144aadcd1ce5b888f8bb913fc4e310
tuned agressiveness of isar compression

diff -r 1491459df114 -r 61bc5a3bef09 src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Sun Feb 24 13:46:14 2013 +1100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Sun Feb 24 15:49:07 2013 +0100
@@ -69,11 +69,10 @@
     end
 
     (* compress top level steps - do not compress subproofs *)
-    fun compress_top_level on_top_level ctxt steps =
+    fun compress_top_level on_top_level ctxt n steps =
     let
       (* proof step vector *)
       val step_vect = steps |> map SOME |> Vector.fromList
-      val n = Vector.length step_vect
       val n_metis = add_metis_steps_top_level steps 0
       val target_n_metis = Real.fromInt n_metis / isar_compress |> Real.round
 
@@ -91,7 +90,7 @@
         | SOME (By_Metis (subproofs, (lfs, _))) =>
             maps (steps_of_proof #> maps refs) subproofs @ lookup_indices lfs)
       val refed_by_vect =
-        Vector.tabulate (n, K [])
+        Vector.tabulate (Vector.length step_vect, K [])
         |> fold_index (fn (i, step) => fold (update (cons i)) (refs step)) steps
         |> Vector.map rev (* after rev, indices are sorted in ascending order *)
 
@@ -202,7 +201,7 @@
       merge_steps metis_time step_vect refed_by_vect cand_tab n n_metis
     end
 
-    fun do_proof on_top_level ctxt (Proof (fix, assms,steps)) =
+    fun do_proof on_top_level ctxt (Proof (Fix fix, Assume assms, steps)) =
       let
         (* Enrich context with top-level facts *)
         val thy = Proof_Context.theory_of ctxt
@@ -214,17 +213,18 @@
           | enrich_with_step (Obtain (_, _, l, t, _)) = enrich_with_fact l t
           | enrich_with_step _ = I
         val enrich_with_steps = fold enrich_with_step
-        fun enrich_with_assms (Assume assms) =
-          fold (uncurry enrich_with_fact) assms
+        val enrich_with_assms = fold (uncurry enrich_with_fact)
         val rich_ctxt =
           ctxt |> enrich_with_assms assms |> enrich_with_steps steps
 
+        val n = List.length fix + List.length assms + List.length steps
+
         (* compress subproofs and top-levl steps *)
         val ((steps, top_level_time), lower_level_time) =
           steps |> do_subproofs rich_ctxt
-                |>> compress_top_level on_top_level rich_ctxt
+                |>> compress_top_level on_top_level rich_ctxt n
       in
-        (Proof (fix, assms, steps),
+        (Proof (Fix fix, Assume assms, steps),
           add_preplay_time lower_level_time top_level_time)
       end