# HG changeset patch
# User smolkas
# Date 1373711920 -7200
# Node ID 21774f0b7bc086280fb599fc3aa46a904be230bf
# Parent  23393c31c7feebaae9ca358fa32818ac60548e4a
tuned

diff -r 23393c31c7fe -r 21774f0b7bc0 src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML
--- 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
diff -r 23393c31c7fe -r 21774f0b7bc0 src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML
--- 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