--- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Fri Jul 12 22:41:25 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Sat Jul 13 12:38:40 2013 +0200
@@ -2,8 +2,8 @@
Author: Jasmin Blanchette, TU Muenchen
Author: Steffen Juilf Smolka, TU Muenchen
-Compression of isar proofs.
-Only proof steps using the MetisM proof_method are compressed.
+Compression of isar proofs by merging steps.
+Only proof steps using the MetisM proof_method are merged.
PRE CONDITION: the proof must be labeled canocially, see
Slegehammer_Proof.relabel_proof_canonically
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Fri Jul 12 22:41:25 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Sat Jul 13 12:38:40 2013 +0200
@@ -115,7 +115,7 @@
|> thm_of_term ctxt
end
-(* mapping of proof methods to tactics *)
+(* mapping from proof methods to tactics *)
fun tac_of_method method type_enc lam_trans ctxt facts =
case method of
MetisM => Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts
@@ -123,7 +123,7 @@
Method.insert_tac facts
THEN' (case method of
SimpM => Simplifier.asm_full_simp_tac
- | AutoM => (fn ctxt => K (Clasimp.auto_tac ctxt))
+ | AutoM => Clasimp.auto_tac #> K
| FastforceM => Clasimp.fast_force_tac
| ForceM => Clasimp.force_tac
| ArithM => Arith_Data.arith_tac