--- a/src/HOL/List.thy Thu Jun 12 17:02:03 2014 +0200
+++ b/src/HOL/List.thy Thu Jun 12 17:02:03 2014 +0200
@@ -5,7 +5,7 @@
header {* The datatype of finite lists *}
theory List
-imports Sledgehammer Code_Numeral Quotient Lifting_Set Lifting_Option Lifting_Product
+imports Sledgehammer Code_Numeral Lifting_Set Lifting_Option Lifting_Product
begin
datatype_new (set: 'a) list =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Thu Jun 12 17:02:03 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Thu Jun 12 17:02:03 2014 +0200
@@ -71,7 +71,7 @@
fun weight_smt_fact ctxt num_facts ((info, th), j) =
let val thy = Proof_Context.theory_of ctxt in
- (info, (smt_fact_weight ctxt j num_facts, Thm.transfer thy th (* TODO: needed? *)))
+ (info, (smt_fact_weight ctxt j num_facts, Thm.transfer thy th))
end
(* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Thu Jun 12 17:02:03 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Thu Jun 12 17:02:03 2014 +0200
@@ -184,6 +184,8 @@
val thy = Proof.theory_of state
val ctxt = Proof.context_of state
+ val factss = map (apsnd (map (apsnd (Thm.transfer thy)))) factss
+
val {outcome, filter_result = {fact_ids, atp_proof, ...}, used_from, run_time} =
smt2_filter_loop name params state goal subgoal factss
val used_named_facts = map snd fact_ids