src/HOL/Tools/res_atp.ML
changeset 27178 c8ddb3000743
parent 26928 ca87aff1ad2d
child 27865 27a8ad9612a3
     1.1 --- a/src/HOL/Tools/res_atp.ML	Thu Jun 12 16:42:00 2008 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Jun 12 18:54:29 2008 +0200
     1.3 @@ -570,8 +570,10 @@
     1.4  (***************************************************************)
     1.5  
     1.6  fun cnf_hyps_thms ctxt =
     1.7 -    let val ths = Assumption.prems_of ctxt
     1.8 -    in fold (fold (insert Thm.eq_thm) o ResAxioms.cnf_axiom) ths [] end;
     1.9 +  let
    1.10 +    val thy = ProofContext.theory_of ctxt
    1.11 +    val hyps = Assumption.prems_of ctxt
    1.12 +  in fold (fold (insert Thm.eq_thm) o ResAxioms.cnf_axiom thy) hyps [] end;
    1.13  
    1.14  (*Translation mode can be auto-detected, or forced to be first-order or higher-order*)
    1.15  datatype mode = Auto | Fol | Hol;
    1.16 @@ -646,10 +648,10 @@
    1.17                            | Hol => false
    1.18          val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
    1.19          val cla_simp_atp_clauses = included_thms
    1.20 -                                     |> ResAxioms.cnf_rules_pairs |> make_unique
    1.21 +                                     |> ResAxioms.cnf_rules_pairs thy |> make_unique
    1.22                                       |> restrict_to_logic thy isFO
    1.23                                       |> remove_unwanted_clauses
    1.24 -        val user_cls = ResAxioms.cnf_rules_pairs user_rules
    1.25 +        val user_cls = ResAxioms.cnf_rules_pairs thy user_rules
    1.26          val axclauses = make_unique (user_cls @ relevance_filter thy cla_simp_atp_clauses goal_tms)
    1.27          val subs = tfree_classes_of_terms goal_tms
    1.28          and axtms = map (prop_of o #1) axclauses
    1.29 @@ -729,11 +731,11 @@
    1.30  			| Fol => true
    1.31  			| Hol => false
    1.32        val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt chain_ths
    1.33 -      val included_cls = included_thms |> ResAxioms.cnf_rules_pairs |> make_unique
    1.34 +      val included_cls = included_thms |> ResAxioms.cnf_rules_pairs thy |> make_unique
    1.35                                         |> restrict_to_logic thy isFO
    1.36                                         |> remove_unwanted_clauses
    1.37        val _ = Output.debug (fn () => "included clauses = " ^ Int.toString(length included_cls))
    1.38 -      val white_cls = ResAxioms.cnf_rules_pairs white_thms
    1.39 +      val white_cls = ResAxioms.cnf_rules_pairs thy white_thms
    1.40        (*clauses relevant to goal gl*)
    1.41        val axcls_list = map (fn ngcls => white_cls @ relevance_filter thy included_cls (map prop_of ngcls)) goal_cls
    1.42        val _ = app (fn axcls => Output.debug (fn () => "filtered clauses = " ^ Int.toString(length axcls)))