# HG changeset patch
# User smolkas
# Date 1354101906 -3600
# Node ID a1a1685b4ee842c68347ab7c17429f897ae78dab
# Parent  87ddf7eddfc91d92ed4030057c4d22fac8655c7b
remove hack and generalize code slightly

diff -r 87ddf7eddfc9 -r a1a1685b4ee8 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Nov 28 12:23:44 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Nov 28 12:25:06 2012 +0100
@@ -709,7 +709,7 @@
           |> redirect_graph axioms tainted
           |> map (do_inf true)
           |> append assms
-          |> relabel_proof (* FIXME: Is there a better way? *)
+          (*|> relabel_proof (* FIXME: Is there a better way? *) *)
           |> (if not preplay andalso isar_shrink <= 1.0
               then pair (true, seconds 0.0) #> swap
               else shrink_proof debug ctxt type_enc lam_trans preplay
diff -r 87ddf7eddfc9 -r a1a1685b4ee8 src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Wed Nov 28 12:23:44 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Wed Nov 28 12:25:06 2012 +0100
@@ -103,7 +103,7 @@
             fact_names
             |>> map string_for_label 
             |> op @
-            |> map (the_single o thms_of_name ctxt) (* FIXME: maps (the o thms_of_name ctxt) *)
+            |> maps (thms_of_name ctxt) (* FIXME: maps (the o thms_of_name ctxt) *)
           val goal =
             Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] t
           fun tac {context = ctxt, prems = _} =