--- a/src/HOL/Tools/metis_tools.ML Thu Jun 12 16:42:00 2008 +0200
+++ b/src/HOL/Tools/metis_tools.ML Thu Jun 12 18:54:29 2008 +0200
@@ -470,16 +470,16 @@
(* Translation of HO Clauses *)
(* ------------------------------------------------------------------------- *)
- fun cnf_th th = hd (ResAxioms.cnf_axiom th);
+ fun cnf_th thy th = hd (ResAxioms.cnf_axiom thy th);
- val equal_imp_fequal' = cnf_th (thm"equal_imp_fequal");
- val fequal_imp_equal' = cnf_th (thm"fequal_imp_equal");
+ val equal_imp_fequal' = cnf_th @{theory} (thm"equal_imp_fequal");
+ val fequal_imp_equal' = cnf_th @{theory} (thm"fequal_imp_equal");
- val comb_I = cnf_th ResHolClause.comb_I;
- val comb_K = cnf_th ResHolClause.comb_K;
- val comb_B = cnf_th ResHolClause.comb_B;
- val comb_C = cnf_th ResHolClause.comb_C;
- val comb_S = cnf_th ResHolClause.comb_S;
+ val comb_I = cnf_th @{theory} ResHolClause.comb_I;
+ val comb_K = cnf_th @{theory} ResHolClause.comb_K;
+ val comb_B = cnf_th @{theory} ResHolClause.comb_B;
+ val comb_C = cnf_th @{theory} ResHolClause.comb_C;
+ val comb_S = cnf_th @{theory} ResHolClause.comb_S;
fun type_ext thy tms =
let val subs = ResAtp.tfree_classes_of_terms tms
@@ -567,7 +567,8 @@
(* Main function to start metis prove and reconstruction *)
fun FOL_SOLVE mode ctxt cls ths0 =
- let val th_cls_pairs = map (fn th => (PureThy.get_name_hint th, ResAxioms.cnf_axiom th)) ths0
+ let val thy = ProofContext.theory_of ctxt
+ val th_cls_pairs = map (fn th => (PureThy.get_name_hint th, ResAxioms.cnf_axiom thy th)) ths0
val ths = List.concat (map #2 th_cls_pairs)
val _ = if exists(is_false o prop_of) cls then error "problem contains the empty clause"
else ();
--- a/src/HOL/Tools/res_atp.ML Thu Jun 12 16:42:00 2008 +0200
+++ b/src/HOL/Tools/res_atp.ML Thu Jun 12 18:54:29 2008 +0200
@@ -570,8 +570,10 @@
(***************************************************************)
fun cnf_hyps_thms ctxt =
- let val ths = Assumption.prems_of ctxt
- in fold (fold (insert Thm.eq_thm) o ResAxioms.cnf_axiom) ths [] end;
+ let
+ val thy = ProofContext.theory_of ctxt
+ val hyps = Assumption.prems_of ctxt
+ in fold (fold (insert Thm.eq_thm) o ResAxioms.cnf_axiom thy) hyps [] end;
(*Translation mode can be auto-detected, or forced to be first-order or higher-order*)
datatype mode = Auto | Fol | Hol;
@@ -646,10 +648,10 @@
| Hol => false
val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
val cla_simp_atp_clauses = included_thms
- |> ResAxioms.cnf_rules_pairs |> make_unique
+ |> ResAxioms.cnf_rules_pairs thy |> make_unique
|> restrict_to_logic thy isFO
|> remove_unwanted_clauses
- val user_cls = ResAxioms.cnf_rules_pairs user_rules
+ val user_cls = ResAxioms.cnf_rules_pairs thy user_rules
val axclauses = make_unique (user_cls @ relevance_filter thy cla_simp_atp_clauses goal_tms)
val subs = tfree_classes_of_terms goal_tms
and axtms = map (prop_of o #1) axclauses
@@ -729,11 +731,11 @@
| Fol => true
| Hol => false
val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt chain_ths
- val included_cls = included_thms |> ResAxioms.cnf_rules_pairs |> make_unique
+ val included_cls = included_thms |> ResAxioms.cnf_rules_pairs thy |> make_unique
|> restrict_to_logic thy isFO
|> remove_unwanted_clauses
val _ = Output.debug (fn () => "included clauses = " ^ Int.toString(length included_cls))
- val white_cls = ResAxioms.cnf_rules_pairs white_thms
+ val white_cls = ResAxioms.cnf_rules_pairs thy white_thms
(*clauses relevant to goal gl*)
val axcls_list = map (fn ngcls => white_cls @ relevance_filter thy included_cls (map prop_of ngcls)) goal_cls
val _ = app (fn axcls => Output.debug (fn () => "filtered clauses = " ^ Int.toString(length axcls)))
--- a/src/HOL/Tools/res_hol_clause.ML Thu Jun 12 16:42:00 2008 +0200
+++ b/src/HOL/Tools/res_hol_clause.ML Thu Jun 12 18:54:29 2008 +0200
@@ -395,7 +395,8 @@
if axiom_name mem_string user_lemmas then foldl count_literal ct literals
else ct;
-val cnf_helper_thms = ResAxioms.cnf_rules_pairs o (map ResAxioms.pairname)
+fun cnf_helper_thms thy =
+ ResAxioms.cnf_rules_pairs thy o map ResAxioms.pairname
fun get_helper_clauses thy isFO (conjectures, axclauses, user_lemmas) =
if isFO then [] (*first-order*)
@@ -404,15 +405,15 @@
val ct = foldl (count_user_clause user_lemmas) ct0 axclauses
fun needed c = valOf (Symtab.lookup ct c) > 0
val IK = if needed "c_COMBI" orelse needed "c_COMBK"
- then (Output.debug (fn () => "Include combinator I K"); cnf_helper_thms [comb_I,comb_K])
+ then (Output.debug (fn () => "Include combinator I K"); cnf_helper_thms thy [comb_I,comb_K])
else []
val BC = if needed "c_COMBB" orelse needed "c_COMBC"
- then (Output.debug (fn () => "Include combinator B C"); cnf_helper_thms [comb_B,comb_C])
+ then (Output.debug (fn () => "Include combinator B C"); cnf_helper_thms thy [comb_B,comb_C])
else []
val S = if needed "c_COMBS"
- then (Output.debug (fn () => "Include combinator S"); cnf_helper_thms [comb_S])
+ then (Output.debug (fn () => "Include combinator S"); cnf_helper_thms thy [comb_S])
else []
- val other = cnf_helper_thms [ext,fequal_imp_equal,equal_imp_fequal]
+ val other = cnf_helper_thms thy [ext,fequal_imp_equal,equal_imp_fequal]
in
map #2 (make_axiom_clauses thy (other @ IK @ BC @ S))
end;