src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML
changeset 56984 d20f19f54789
parent 56983 132142089ea6
child 56985 82c83978fbd9
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Fri May 16 19:13:50 2014 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Fri May 16 19:13:50 2014 +0200
     1.3 @@ -71,9 +71,7 @@
     1.4      NONE
     1.5  
     1.6  fun weight_smt2_fact ctxt num_facts ((info, th), j) =
     1.7 -  let val thy = Proof_Context.theory_of ctxt in
     1.8 -    (info, (smt2_fact_weight ctxt j num_facts, Thm.transfer thy th (* TODO: needed? *)))
     1.9 -  end
    1.10 +  (info, (smt2_fact_weight ctxt j num_facts, th))
    1.11  
    1.12  (* "SMT2_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out
    1.13     properly in the SMT module, we must interpret these here. *)