# HG changeset patch
# User blanchet
# Date 1350560273 -7200
# Node ID e88a864fa35ce20a252db48ad2ab5edb3779883c
# Parent  23e36a4d28f1dab28c3dd5078052fcf7993f949b
tuning

diff -r 23e36a4d28f1 -r e88a864fa35c src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Oct 18 13:19:44 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Oct 18 13:37:53 2012 +0200
@@ -751,7 +751,7 @@
 
     (* Enrich context with facts *)
     val thy = Proof_Context.theory_of ctxt
-    fun sorry t = Skip_Proof.make_thm thy (HOLogic.mk_Trueprop t) (* FIXME: mk_Trueprop always ok? *)
+    fun sorry t = Skip_Proof.make_thm thy (HOLogic.mk_Trueprop t)
     fun enrich_ctxt' (Prove (_, lbl, t, _)) ctxt = 
         ctxt |> lbl <> no_label
           ? Proof_Context.put_thms false (string_for_label lbl, SOME [sorry t])
@@ -760,21 +760,18 @@
 
     (* Timing *)
     fun take_time tac arg =
-      let
-        val t_start = Timing.start ()
-      in
-        (tac arg ; Timing.result t_start |> #cpu)
+      let val t_start = Timing.start () in
+        (tac arg; Timing.result t_start |> #cpu)
       end
     fun try_metis (Prove (qs, _, t, By_Metis fact_names)) s0 =
       let
         fun thmify (Prove (_, _, t, _)) = sorry t
         val facts =
           fact_names
-          |>> map string_for_label
-          |> op @
+          |>> map string_for_label |> op @
           |> map (Proof_Context.get_thm rich_ctxt)
           |> (if member (op =) qs Then then cons (the s0 |> thmify) else I)
-        val goal = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop t) (* FIXME: mk_Trueprop always ok? *)
+        val goal = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop t)
         fun tac {context = ctxt, prems = _} =
           Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1
       in
@@ -805,9 +802,7 @@
         val tlimit = t1 + t2 |> Time.toReal |> curry Real.* 1.2 |> Time.fromReal
       in
         (TimeLimit.timeLimit tlimit (try_metis s12 s0) ();
-         SOME (front @ (case s0 of
-                          NONE => s12 :: tail
-                        | SOME s => s :: s12 :: tail)))
+         SOME (front @ (the_list s0 @ s12 :: tail)))
         handle _ => NONE
       end
     fun merge_steps proof [] = proof