src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML
changeset 57243 8c261f0a9b32
parent 57165 7b1bf424ec5f
child 57245 f6bf6d5341ee
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Thu Jun 12 17:02:03 2014 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Thu Jun 12 17:02:03 2014 +0200
     1.3 @@ -184,6 +184,8 @@
     1.4      val thy = Proof.theory_of state
     1.5      val ctxt = Proof.context_of state
     1.6  
     1.7 +    val factss = map (apsnd (map (apsnd (Thm.transfer thy)))) factss
     1.8 +
     1.9      val {outcome, filter_result = {fact_ids, atp_proof, ...}, used_from, run_time} =
    1.10        smt2_filter_loop name params state goal subgoal factss
    1.11      val used_named_facts = map snd fact_ids