# HG changeset patch
# User smolkas
# Date 1354101606 -3600
# Node ID ed9487289e04e748f22cc863a79295a13dd715f3
# Parent  3f0920f8a24eeb30ccb843424ffadb59abeed39f
some minor improvements in shrink_proof

diff -r 3f0920f8a24e -r ed9487289e04 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Nov 27 20:01:57 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Nov 28 12:20:06 2012 +0100
@@ -799,11 +799,11 @@
 
     (* Enrich context with local facts *)
     val thy = Proof_Context.theory_of ctxt
-    fun enrich_ctxt' (Prove (_, label, t, _)) ctxt =
+    fun enrich_ctxt (Prove (_, label, t, _)) ctxt =
         Proof_Context.put_thms false
             (string_for_label label, SOME [Skip_Proof.make_thm thy t]) ctxt
-      | enrich_ctxt' _ ctxt = ctxt
-    val rich_ctxt = fold enrich_ctxt' proof ctxt
+      | enrich_ctxt _ ctxt = ctxt
+    val rich_ctxt = fold enrich_ctxt proof ctxt
 
     (* Timing *)
     fun take_time timeout tac arg =