reintroduced vital 'Thm.transfer'
authorblanchet
Thu Jun 12 17:02:03 2014 +0200 (2014-06-12 ago)
changeset 572438c261f0a9b32
parent 57242 25aff3b8d550
child 57244 ee08e7b8ad2b
reintroduced vital 'Thm.transfer'
src/HOL/List.thy
src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML
     1.1 --- a/src/HOL/List.thy	Thu Jun 12 17:02:03 2014 +0200
     1.2 +++ b/src/HOL/List.thy	Thu Jun 12 17:02:03 2014 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* The datatype of finite lists *}
     1.5  
     1.6  theory List
     1.7 -imports Sledgehammer Code_Numeral Quotient Lifting_Set Lifting_Option Lifting_Product
     1.8 +imports Sledgehammer Code_Numeral Lifting_Set Lifting_Option Lifting_Product
     1.9  begin
    1.10  
    1.11  datatype_new (set: 'a) list =
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Thu Jun 12 17:02:03 2014 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Thu Jun 12 17:02:03 2014 +0200
     2.3 @@ -71,7 +71,7 @@
     2.4  
     2.5  fun weight_smt_fact ctxt num_facts ((info, th), j) =
     2.6    let val thy = Proof_Context.theory_of ctxt in
     2.7 -    (info, (smt_fact_weight ctxt j num_facts, Thm.transfer thy th (* TODO: needed? *)))
     2.8 +    (info, (smt_fact_weight ctxt j num_facts, Thm.transfer thy th))
     2.9    end
    2.10  
    2.11  (* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Thu Jun 12 17:02:03 2014 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Thu Jun 12 17:02:03 2014 +0200
     3.3 @@ -184,6 +184,8 @@
     3.4      val thy = Proof.theory_of state
     3.5      val ctxt = Proof.context_of state
     3.6  
     3.7 +    val factss = map (apsnd (map (apsnd (Thm.transfer thy)))) factss
     3.8 +
     3.9      val {outcome, filter_result = {fact_ids, atp_proof, ...}, used_from, run_time} =
    3.10        smt2_filter_loop name params state goal subgoal factss
    3.11      val used_named_facts = map snd fact_ids