--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Fri May 16 19:13:50 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Fri May 16 19:14:00 2014 +0200
@@ -246,7 +246,8 @@
map (fn (id, th) => (id, short_thm_name ctxt th)) helper_ids @
map (fn (id, ((name, _), _)) => (id, name)) fact_ids
val atp_proof = Z3_New_Isar.atp_proof_of_z3_proof ctxt rewrite_rules hyp_ts concl_t
- prem_ids conjecture_id fact_ids z3_proof
+ (map (fn ((s, _), th) => (s, prop_of th)) used_named_facts) prem_ids conjecture_id
+ fact_ids z3_proof
val isar_params =
K (verbose, (NONE, NONE), preplay_timeout, compress_isar, try0_isar,
minimize <> SOME false, atp_proof, goal)