--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Sep 20 22:39:30 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Sep 20 22:39:30 2013 +0200
@@ -12,9 +12,9 @@
type one_line_params = Sledgehammer_Print.one_line_params
type isar_params =
- bool * bool * Time.time option * real * int * bool * bool
- * string Symtab.table * (string * stature) list vector
- * (string * term) list * int Symtab.table * string atp_proof * thm
+ bool * bool * Time.time option * real * bool * bool * string Symtab.table
+ * (string * stature) list vector * (string * term) list * int Symtab.table
+ * string atp_proof * thm
val lam_trans_of_atp_proof : string atp_proof -> string -> string
val is_typed_helper_used_in_atp_proof : string atp_proof -> bool
@@ -408,14 +408,13 @@
in chain_proof end
type isar_params =
- bool * bool * Time.time option * real * int * bool * bool
- * string Symtab.table * (string * stature) list vector
- * (string * term) list * int Symtab.table * string atp_proof * thm
+ bool * bool * Time.time option * real * bool * bool * string Symtab.table
+ * (string * stature) list vector * (string * term) list * int Symtab.table
+ * string atp_proof * thm
fun isar_proof_text ctxt isar_proofs
- (debug, verbose, preplay_timeout, isar_compress, isar_compress_degree,
- isar_try0, isar_minimize, pool, fact_names, lifted, sym_tab, atp_proof,
- goal)
+ (debug, verbose, preplay_timeout, isar_compress, isar_try0, isar_minimize,
+ pool, fact_names, lifted, sym_tab, atp_proof, goal)
(one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
let
val (params, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt
@@ -591,7 +590,6 @@
isar_proof
|> compress_proof
(if isar_proofs = SOME true then isar_compress else 1000.0)
- (if isar_proofs = SOME true then isar_compress_degree else 100)
preplay_interface
|> isar_try0 ? try0 preplay_timeout preplay_interface
|> minimize_dependencies_and_remove_unrefed_steps isar_minimize