--- 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
--- 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 = _} =