# HG changeset patch # User blanchet # Date 1400260430 -7200 # Node ID d20f19f54789414be3db14f5aec129a3a97cf84a # Parent 132142089ea65678236c0c4c884cba47d9ef1ac9 removed needless transfer diff -r 132142089ea6 -r d20f19f54789 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML --- 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:13:50 2014 +0200 @@ -71,9 +71,7 @@ NONE fun weight_smt2_fact ctxt num_facts ((info, th), j) = - let val thy = Proof_Context.theory_of ctxt in - (info, (smt2_fact_weight ctxt j num_facts, Thm.transfer thy th (* TODO: needed? *))) - end + (info, (smt2_fact_weight ctxt j num_facts, th)) (* "SMT2_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out properly in the SMT module, we must interpret these here. *)