# HG changeset patch
# User blanchet
# Date 1352197488 -3600
# Node ID 3bb634c9fedb3a7d69ca4aa7d4c63599f8c892ac
# Parent  cceec179bdca09bece5b5c9a44d2bc77b928b9fe
avoid double "Trueprop"s

diff -r cceec179bdca -r 3bb634c9fedb src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Nov 06 11:20:56 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Nov 06 11:24:48 2012 +0100
@@ -799,10 +799,9 @@
 
     (* Enrich context with local facts *)
     val thy = Proof_Context.theory_of ctxt
-    fun sorry t = Skip_Proof.make_thm thy (HOLogic.mk_Trueprop t)
     fun enrich_ctxt' (Prove (_, label, t, _)) ctxt =
-        Proof_Context.put_thms false (string_for_label label, SOME [sorry 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
 
@@ -827,8 +826,8 @@
             fact_names
             |>> map string_for_label |> op @
             |> map (the_single o thms_of_name rich_ctxt)
-          val goal = Goal.prove (Config.put Metis_Tactic.verbose debug ctxt)
-            [] [] (HOLogic.mk_Trueprop t)
+          val goal =
+            Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] t
           fun tac {context = ctxt, prems = _} =
             Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1
         in