--- a/src/HOL/ATP_Linkup.thy Thu Oct 29 16:34:44 2009 +0100
+++ b/src/HOL/ATP_Linkup.thy Thu Oct 29 16:59:12 2009 +0100
@@ -91,9 +91,9 @@
subsection {* Setup of external ATPs *}
-use "Tools/res_axioms.ML" setup ResAxioms.setup
+use "Tools/res_axioms.ML" setup Res_Axioms.setup
use "Tools/res_hol_clause.ML"
-use "Tools/res_reconstruct.ML" setup ResReconstruct.setup
+use "Tools/res_reconstruct.ML" setup Res_Reconstruct.setup
use "Tools/res_atp.ML"
use "Tools/ATP_Manager/atp_wrapper.ML" setup ATP_Wrapper.setup
--- a/src/HOL/HOL.thy Thu Oct 29 16:34:44 2009 +0100
+++ b/src/HOL/HOL.thy Thu Oct 29 16:59:12 2009 +0100
@@ -35,7 +35,8 @@
begin
setup {* Intuitionistic.method_setup @{binding iprover} *}
-setup ResBlacklist.setup
+
+setup Res_Blacklist.setup
subsection {* Primitive logic *}
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Oct 29 16:34:44 2009 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Oct 29 16:59:12 2009 +0100
@@ -319,7 +319,7 @@
if success then (message, SH_OK (time_isa, time_atp, theorem_names))
else (message, SH_FAIL(time_isa, time_atp))
end
- handle ResHolClause.TOO_TRIVIAL => ("trivial", SH_OK (0, 0, []))
+ handle Res_HOL_Clause.TOO_TRIVIAL => ("trivial", SH_OK (0, 0, []))
| ERROR msg => ("error: " ^ msg, SH_ERROR)
| TimeLimit.TimeOut => ("timeout", SH_ERROR)
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Thu Oct 29 16:34:44 2009 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Thu Oct 29 16:59:12 2009 +0100
@@ -264,7 +264,7 @@
val _ = register birth_time death_time (Thread.self (), desc);
val problem = ATP_Wrapper.problem_of_goal (! full_types) i (ctxt, (facts, goal));
val message = #message (prover (! timeout) problem)
- handle ResHolClause.TOO_TRIVIAL => (* FIXME !? *)
+ handle Res_HOL_Clause.TOO_TRIVIAL => (* FIXME !? *)
"Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis"
| ERROR msg => ("Error: " ^ msg);
val _ = unregister message (Thread.self ());
--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Thu Oct 29 16:34:44 2009 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Thu Oct 29 16:59:12 2009 +0100
@@ -103,7 +103,7 @@
let
val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^ " theorems... ")
val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
- val axclauses = ResAxioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
+ val axclauses = Res_Axioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
val {context = ctxt, facts, goal} = Proof.raw_goal state (* FIXME ?? *)
val problem =
{with_full_types = ! ATP_Manager.full_types,
@@ -157,7 +157,7 @@
(NONE, "Error in prover: " ^ msg)
| (Failure, _) =>
(NONE, "Failure: No proof with the theorems supplied"))
- handle ResHolClause.TOO_TRIVIAL =>
+ handle Res_HOL_Clause.TOO_TRIVIAL =>
(SOME ([], 0), "Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
| ERROR msg => (NONE, "Error: " ^ msg)
end
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Thu Oct 29 16:34:44 2009 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Thu Oct 29 16:59:12 2009 +0100
@@ -117,8 +117,8 @@
(* get clauses and prepare them for writing *)
val (ctxt, (chain_ths, th)) = goal;
val thy = ProofContext.theory_of ctxt;
- val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths;
- val goal_cls = #1 (ResAxioms.neg_conjecture_clauses ctxt th subgoalno);
+ val chain_ths = map (Thm.put_name_hint Res_Reconstruct.chained_hint) chain_ths;
+ val goal_cls = #1 (Res_Axioms.neg_conjecture_clauses ctxt th subgoalno);
val the_filtered_clauses =
(case filtered_clauses of
NONE => relevance_filter goal goal_cls
@@ -204,14 +204,14 @@
val {with_full_types, subgoal, goal, axiom_clauses, filtered_clauses} = problem;
in
external_prover
- (ResAtp.get_relevant max_new_clauses insert_theory_const)
- (ResAtp.prepare_clauses false)
- (ResHolClause.tptp_write_file with_full_types)
+ (Res_ATP.get_relevant max_new_clauses insert_theory_const)
+ (Res_ATP.prepare_clauses false)
+ (Res_HOL_Clause.tptp_write_file with_full_types)
command
(arguments timeout)
- ResReconstruct.find_failure
- (if emit_structured_proof then ResReconstruct.structured_proof
- else ResReconstruct.lemma_list false)
+ Res_Reconstruct.find_failure
+ (if emit_structured_proof then Res_Reconstruct.structured_proof
+ else Res_Reconstruct.lemma_list false)
axiom_clauses
filtered_clauses
name
@@ -280,13 +280,13 @@
val {with_full_types, subgoal, goal, axiom_clauses, filtered_clauses} = problem
in
external_prover
- (ResAtp.get_relevant max_new_clauses insert_theory_const)
- (ResAtp.prepare_clauses true)
- (ResHolClause.dfg_write_file with_full_types)
+ (Res_ATP.get_relevant max_new_clauses insert_theory_const)
+ (Res_ATP.prepare_clauses true)
+ (Res_HOL_Clause.dfg_write_file with_full_types)
command
(arguments timeout)
- ResReconstruct.find_failure
- (ResReconstruct.lemma_list true)
+ Res_Reconstruct.find_failure
+ (Res_Reconstruct.lemma_list true)
axiom_clauses
filtered_clauses
name
--- a/src/HOL/Tools/metis_tools.ML Thu Oct 29 16:34:44 2009 +0100
+++ b/src/HOL/Tools/metis_tools.ML Thu Oct 29 16:59:12 2009 +0100
@@ -63,62 +63,62 @@
fun metis_lit b c args = (b, (c, args));
-fun hol_type_to_fol (ResClause.AtomV x) = Metis.Term.Var x
- | hol_type_to_fol (ResClause.AtomF x) = Metis.Term.Fn(x,[])
- | hol_type_to_fol (ResClause.Comp(tc,tps)) = Metis.Term.Fn(tc, map hol_type_to_fol tps);
+fun hol_type_to_fol (Res_Clause.AtomV x) = Metis.Term.Var x
+ | hol_type_to_fol (Res_Clause.AtomF x) = Metis.Term.Fn(x,[])
+ | hol_type_to_fol (Res_Clause.Comp(tc,tps)) = Metis.Term.Fn(tc, map hol_type_to_fol tps);
(*These two functions insert type literals before the real literals. That is the
opposite order from TPTP linkup, but maybe OK.*)
fun hol_term_to_fol_FO tm =
- case ResHolClause.strip_comb tm of
- (ResHolClause.CombConst(c,_,tys), tms) =>
+ case Res_HOL_Clause.strip_comb tm of
+ (Res_HOL_Clause.CombConst(c,_,tys), tms) =>
let val tyargs = map hol_type_to_fol tys
val args = map hol_term_to_fol_FO tms
in Metis.Term.Fn (c, tyargs @ args) end
- | (ResHolClause.CombVar(v,_), []) => Metis.Term.Var v
+ | (Res_HOL_Clause.CombVar(v,_), []) => Metis.Term.Var v
| _ => error "hol_term_to_fol_FO";
-fun hol_term_to_fol_HO (ResHolClause.CombVar (a, _)) = Metis.Term.Var a
- | hol_term_to_fol_HO (ResHolClause.CombConst (a, _, tylist)) =
+fun hol_term_to_fol_HO (Res_HOL_Clause.CombVar (a, _)) = Metis.Term.Var a
+ | hol_term_to_fol_HO (Res_HOL_Clause.CombConst (a, _, tylist)) =
Metis.Term.Fn (fn_isa_to_met a, map hol_type_to_fol tylist)
- | hol_term_to_fol_HO (ResHolClause.CombApp (tm1, tm2)) =
+ | hol_term_to_fol_HO (Res_HOL_Clause.CombApp (tm1, tm2)) =
Metis.Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
(*The fully-typed translation, to avoid type errors*)
fun wrap_type (tm, ty) = Metis.Term.Fn("ti", [tm, hol_type_to_fol ty]);
-fun hol_term_to_fol_FT (ResHolClause.CombVar(a, ty)) =
+fun hol_term_to_fol_FT (Res_HOL_Clause.CombVar(a, ty)) =
wrap_type (Metis.Term.Var a, ty)
- | hol_term_to_fol_FT (ResHolClause.CombConst(a, ty, _)) =
+ | hol_term_to_fol_FT (Res_HOL_Clause.CombConst(a, ty, _)) =
wrap_type (Metis.Term.Fn(fn_isa_to_met a, []), ty)
- | hol_term_to_fol_FT (tm as ResHolClause.CombApp(tm1,tm2)) =
+ | hol_term_to_fol_FT (tm as Res_HOL_Clause.CombApp(tm1,tm2)) =
wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]),
- ResHolClause.type_of_combterm tm);
+ Res_HOL_Clause.type_of_combterm tm);
-fun hol_literal_to_fol FO (ResHolClause.Literal (pol, tm)) =
- let val (ResHolClause.CombConst(p,_,tys), tms) = ResHolClause.strip_comb tm
+fun hol_literal_to_fol FO (Res_HOL_Clause.Literal (pol, tm)) =
+ let val (Res_HOL_Clause.CombConst(p,_,tys), tms) = Res_HOL_Clause.strip_comb tm
val tylits = if p = "equal" then [] else map hol_type_to_fol tys
val lits = map hol_term_to_fol_FO tms
in metis_lit pol (fn_isa_to_met p) (tylits @ lits) end
- | hol_literal_to_fol HO (ResHolClause.Literal (pol, tm)) =
- (case ResHolClause.strip_comb tm of
- (ResHolClause.CombConst("equal",_,_), tms) =>
+ | hol_literal_to_fol HO (Res_HOL_Clause.Literal (pol, tm)) =
+ (case Res_HOL_Clause.strip_comb tm of
+ (Res_HOL_Clause.CombConst("equal",_,_), tms) =>
metis_lit pol "=" (map hol_term_to_fol_HO tms)
| _ => metis_lit pol "{}" [hol_term_to_fol_HO tm]) (*hBOOL*)
- | hol_literal_to_fol FT (ResHolClause.Literal (pol, tm)) =
- (case ResHolClause.strip_comb tm of
- (ResHolClause.CombConst("equal",_,_), tms) =>
+ | hol_literal_to_fol FT (Res_HOL_Clause.Literal (pol, tm)) =
+ (case Res_HOL_Clause.strip_comb tm of
+ (Res_HOL_Clause.CombConst("equal",_,_), tms) =>
metis_lit pol "=" (map hol_term_to_fol_FT tms)
| _ => metis_lit pol "{}" [hol_term_to_fol_FT tm]) (*hBOOL*);
fun literals_of_hol_thm thy mode t =
- let val (lits, types_sorts) = ResHolClause.literals_of_term thy t
+ let val (lits, types_sorts) = Res_HOL_Clause.literals_of_term thy t
in (map (hol_literal_to_fol mode) lits, types_sorts) end;
(*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
-fun metis_of_typeLit pos (ResClause.LTVar (s,x)) = metis_lit pos s [Metis.Term.Var x]
- | metis_of_typeLit pos (ResClause.LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])];
+fun metis_of_typeLit pos (Res_Clause.LTVar (s,x)) = metis_lit pos s [Metis.Term.Var x]
+ | metis_of_typeLit pos (Res_Clause.LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])];
fun default_sort _ (TVar _) = false
| default_sort ctxt (TFree (x, s)) = (s = the_default [] (Variable.def_sort ctxt (x, ~1)));
@@ -132,9 +132,9 @@
(literals_of_hol_thm thy mode o HOLogic.dest_Trueprop o prop_of) th
in
if is_conjecture then
- (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), ResClause.add_typs types_sorts)
+ (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), Res_Clause.add_typs types_sorts)
else
- let val tylits = ResClause.add_typs
+ let val tylits = Res_Clause.add_typs
(filter (not o default_sort ctxt) types_sorts)
val mtylits = if Config.get ctxt type_lits
then map (metis_of_typeLit false) tylits else []
@@ -145,13 +145,13 @@
(* ARITY CLAUSE *)
-fun m_arity_cls (ResClause.TConsLit (c,t,args)) =
- metis_lit true (ResClause.make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)]
- | m_arity_cls (ResClause.TVarLit (c,str)) =
- metis_lit false (ResClause.make_type_class c) [Metis.Term.Var str];
+fun m_arity_cls (Res_Clause.TConsLit (c,t,args)) =
+ metis_lit true (Res_Clause.make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)]
+ | m_arity_cls (Res_Clause.TVarLit (c,str)) =
+ metis_lit false (Res_Clause.make_type_class c) [Metis.Term.Var str];
(*TrueI is returned as the Isabelle counterpart because there isn't any.*)
-fun arity_cls (ResClause.ArityClause{conclLit,premLits,...}) =
+fun arity_cls (Res_Clause.ArityClause{conclLit,premLits,...}) =
(TrueI,
Metis.Thm.axiom (Metis.LiteralSet.fromList (map m_arity_cls (conclLit :: premLits))));
@@ -160,7 +160,7 @@
fun m_classrel_cls subclass superclass =
[metis_lit false subclass [Metis.Term.Var "T"], metis_lit true superclass [Metis.Term.Var "T"]];
-fun classrel_cls (ResClause.ClassrelClause {subclass, superclass, ...}) =
+fun classrel_cls (Res_Clause.ClassrelClause {subclass, superclass, ...}) =
(TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (m_classrel_cls subclass superclass)));
(* ------------------------------------------------------------------------- *)
@@ -209,14 +209,14 @@
| strip_happ args x = (x, args);
fun fol_type_to_isa _ (Metis.Term.Var v) =
- (case ResReconstruct.strip_prefix ResClause.tvar_prefix v of
- SOME w => ResReconstruct.make_tvar w
- | NONE => ResReconstruct.make_tvar v)
+ (case Res_Reconstruct.strip_prefix Res_Clause.tvar_prefix v of
+ SOME w => Res_Reconstruct.make_tvar w
+ | NONE => Res_Reconstruct.make_tvar v)
| fol_type_to_isa ctxt (Metis.Term.Fn(x, tys)) =
- (case ResReconstruct.strip_prefix ResClause.tconst_prefix x of
- SOME tc => Term.Type (ResReconstruct.invert_type_const tc, map (fol_type_to_isa ctxt) tys)
+ (case Res_Reconstruct.strip_prefix Res_Clause.tconst_prefix x of
+ SOME tc => Term.Type (Res_Reconstruct.invert_type_const tc, map (fol_type_to_isa ctxt) tys)
| NONE =>
- case ResReconstruct.strip_prefix ResClause.tfree_prefix x of
+ case Res_Reconstruct.strip_prefix Res_Clause.tfree_prefix x of
SOME tf => mk_tfree ctxt tf
| NONE => error ("fol_type_to_isa: " ^ x));
@@ -225,10 +225,10 @@
let val thy = ProofContext.theory_of ctxt
val _ = trace_msg (fn () => "fol_term_to_hol: " ^ Metis.Term.toString fol_tm)
fun tm_to_tt (Metis.Term.Var v) =
- (case ResReconstruct.strip_prefix ResClause.tvar_prefix v of
- SOME w => Type (ResReconstruct.make_tvar w)
+ (case Res_Reconstruct.strip_prefix Res_Clause.tvar_prefix v of
+ SOME w => Type (Res_Reconstruct.make_tvar w)
| NONE =>
- case ResReconstruct.strip_prefix ResClause.schematic_var_prefix v of
+ case Res_Reconstruct.strip_prefix Res_Clause.schematic_var_prefix v of
SOME w => Term (mk_var (w, HOLogic.typeT))
| NONE => Term (mk_var (v, HOLogic.typeT)) )
(*Var from Metis with a name like _nnn; possibly a type variable*)
@@ -245,14 +245,14 @@
and applic_to_tt ("=",ts) =
Term (list_comb(Const ("op =", HOLogic.typeT), terms_of (map tm_to_tt ts)))
| applic_to_tt (a,ts) =
- case ResReconstruct.strip_prefix ResClause.const_prefix a of
+ case Res_Reconstruct.strip_prefix Res_Clause.const_prefix a of
SOME b =>
- let val c = ResReconstruct.invert_const b
- val ntypes = ResReconstruct.num_typargs thy c
+ let val c = Res_Reconstruct.invert_const b
+ val ntypes = Res_Reconstruct.num_typargs thy c
val nterms = length ts - ntypes
val tts = map tm_to_tt ts
val tys = types_of (List.take(tts,ntypes))
- val ntyargs = ResReconstruct.num_typargs thy c
+ val ntyargs = Res_Reconstruct.num_typargs thy c
in if length tys = ntyargs then
apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes))
else error ("Constant " ^ c ^ " expects " ^ Int.toString ntyargs ^
@@ -263,14 +263,14 @@
cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
end
| NONE => (*Not a constant. Is it a type constructor?*)
- case ResReconstruct.strip_prefix ResClause.tconst_prefix a of
+ case Res_Reconstruct.strip_prefix Res_Clause.tconst_prefix a of
SOME b =>
- Type (Term.Type (ResReconstruct.invert_type_const b, types_of (map tm_to_tt ts)))
+ Type (Term.Type (Res_Reconstruct.invert_type_const b, types_of (map tm_to_tt ts)))
| NONE => (*Maybe a TFree. Should then check that ts=[].*)
- case ResReconstruct.strip_prefix ResClause.tfree_prefix a of
+ case Res_Reconstruct.strip_prefix Res_Clause.tfree_prefix a of
SOME b => Type (mk_tfree ctxt b)
| NONE => (*a fixed variable? They are Skolem functions.*)
- case ResReconstruct.strip_prefix ResClause.fixed_var_prefix a of
+ case Res_Reconstruct.strip_prefix Res_Clause.fixed_var_prefix a of
SOME b =>
let val opr = Term.Free(b, HOLogic.typeT)
in apply_list opr (length ts) (map tm_to_tt ts) end
@@ -281,16 +281,16 @@
fun fol_term_to_hol_FT ctxt fol_tm =
let val _ = trace_msg (fn () => "fol_term_to_hol_FT: " ^ Metis.Term.toString fol_tm)
fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) =
- (case ResReconstruct.strip_prefix ResClause.schematic_var_prefix v of
+ (case Res_Reconstruct.strip_prefix Res_Clause.schematic_var_prefix v of
SOME w => mk_var(w, dummyT)
| NONE => mk_var(v, dummyT))
| cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) =
Const ("op =", HOLogic.typeT)
| cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
- (case ResReconstruct.strip_prefix ResClause.const_prefix x of
- SOME c => Const (ResReconstruct.invert_const c, dummyT)
+ (case Res_Reconstruct.strip_prefix Res_Clause.const_prefix x of
+ SOME c => Const (Res_Reconstruct.invert_const c, dummyT)
| NONE => (*Not a constant. Is it a fixed variable??*)
- case ResReconstruct.strip_prefix ResClause.fixed_var_prefix x of
+ case Res_Reconstruct.strip_prefix Res_Clause.fixed_var_prefix x of
SOME v => Free (v, fol_type_to_isa ctxt ty)
| NONE => error ("fol_term_to_hol_FT bad constant: " ^ x))
| cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) =
@@ -301,10 +301,10 @@
| cvt (Metis.Term.Fn ("=", [tm1,tm2])) =
list_comb(Const ("op =", HOLogic.typeT), map cvt [tm1,tm2])
| cvt (t as Metis.Term.Fn (x, [])) =
- (case ResReconstruct.strip_prefix ResClause.const_prefix x of
- SOME c => Const (ResReconstruct.invert_const c, dummyT)
+ (case Res_Reconstruct.strip_prefix Res_Clause.const_prefix x of
+ SOME c => Const (Res_Reconstruct.invert_const c, dummyT)
| NONE => (*Not a constant. Is it a fixed variable??*)
- case ResReconstruct.strip_prefix ResClause.fixed_var_prefix x of
+ case Res_Reconstruct.strip_prefix Res_Clause.fixed_var_prefix x of
SOME v => Free (v, dummyT)
| NONE => (trace_msg (fn () => "fol_term_to_hol_FT bad const: " ^ x);
fol_term_to_hol_RAW ctxt t))
@@ -383,9 +383,9 @@
" in " ^ Display.string_of_thm ctxt i_th);
NONE)
fun remove_typeinst (a, t) =
- case ResReconstruct.strip_prefix ResClause.schematic_var_prefix a of
+ case Res_Reconstruct.strip_prefix Res_Clause.schematic_var_prefix a of
SOME b => SOME (b, t)
- | NONE => case ResReconstruct.strip_prefix ResClause.tvar_prefix a of
+ | NONE => case Res_Reconstruct.strip_prefix Res_Clause.tvar_prefix a of
SOME _ => NONE (*type instantiations are forbidden!*)
| NONE => SOME (a,t) (*internal Metis var?*)
val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th)
@@ -452,7 +452,7 @@
in cterm_instantiate [(refl_x, c_t)] REFL_THM end;
fun get_ty_arg_size _ (Const ("op =", _)) = 0 (*equality has no type arguments*)
- | get_ty_arg_size thy (Const (c, _)) = (ResReconstruct.num_typargs thy c handle TYPE _ => 0)
+ | get_ty_arg_size thy (Const (c, _)) = (Res_Reconstruct.num_typargs thy c handle TYPE _ => 0)
| get_ty_arg_size _ _ = 0;
(* INFERENCE RULE: EQUALITY *)
@@ -538,7 +538,7 @@
| step ctxt mode _ (_, Metis.Proof.Equality (f_lit, f_p, f_r)) =
equality_inf ctxt mode f_lit f_p f_r;
-fun real_literal (_, (c, _)) = not (String.isPrefix ResClause.class_prefix c);
+fun real_literal (_, (c, _)) = not (String.isPrefix Res_Clause.class_prefix c);
fun translate _ _ thpairs [] = thpairs
| translate mode ctxt thpairs ((fol_th, inf) :: infpairs) =
@@ -564,23 +564,23 @@
(* Translation of HO Clauses *)
(* ------------------------------------------------------------------------- *)
-fun cnf_th thy th = hd (ResAxioms.cnf_axiom thy th);
+fun cnf_th thy th = hd (Res_Axioms.cnf_axiom thy th);
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 @{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;
+val comb_I = cnf_th @{theory} Res_HOL_Clause.comb_I;
+val comb_K = cnf_th @{theory} Res_HOL_Clause.comb_K;
+val comb_B = cnf_th @{theory} Res_HOL_Clause.comb_B;
+val comb_C = cnf_th @{theory} Res_HOL_Clause.comb_C;
+val comb_S = cnf_th @{theory} Res_HOL_Clause.comb_S;
fun type_ext thy tms =
- let val subs = ResAtp.tfree_classes_of_terms tms
- val supers = ResAtp.tvar_classes_of_terms tms
- and tycons = ResAtp.type_consts_of_terms thy tms
- val (supers', arity_clauses) = ResClause.make_arity_clauses thy tycons supers
- val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
+ let val subs = Res_ATP.tfree_classes_of_terms tms
+ val supers = Res_ATP.tvar_classes_of_terms tms
+ and tycons = Res_ATP.type_consts_of_terms thy tms
+ val (supers', arity_clauses) = Res_Clause.make_arity_clauses thy tycons supers
+ val classrel_clauses = Res_Clause.make_classrel_clauses thy subs supers'
in map classrel_cls classrel_clauses @ map arity_cls arity_clauses
end;
@@ -590,7 +590,7 @@
type logic_map =
{axioms : (Metis.Thm.thm * thm) list,
- tfrees : ResClause.type_literal list};
+ tfrees : Res_Clause.type_literal list};
fun const_in_metis c (pred, tm_list) =
let
@@ -602,7 +602,7 @@
(*Extract TFree constraints from context to include as conjecture clauses*)
fun init_tfrees ctxt =
let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts
- in ResClause.add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end;
+ in Res_Clause.add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end;
(*transform isabelle type / arity clause to metis clause *)
fun add_type_thm [] lmap = lmap
@@ -664,7 +664,7 @@
(* Main function to start metis prove and reconstruction *)
fun FOL_SOLVE mode ctxt cls ths0 =
let val thy = ProofContext.theory_of ctxt
- val th_cls_pairs = map (fn th => (Thm.get_name_hint th, ResAxioms.cnf_axiom thy th)) ths0
+ val th_cls_pairs = map (fn th => (Thm.get_name_hint th, Res_Axioms.cnf_axiom thy th)) ths0
val ths = maps #2 th_cls_pairs
val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
@@ -673,7 +673,7 @@
val (mode, {axioms,tfrees}) = build_map mode ctxt cls ths
val _ = if null tfrees then ()
else (trace_msg (fn () => "TFREE CLAUSES");
- app (fn tf => trace_msg (fn _ => ResClause.tptp_of_typeLit true tf)) tfrees)
+ app (fn tf => trace_msg (fn _ => Res_Clause.tptp_of_typeLit true tf)) tfrees)
val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS")
val thms = map #1 axioms
val _ = app (fn th => trace_msg (fn () => Metis.Thm.toString th)) thms
@@ -715,12 +715,12 @@
let val _ = trace_msg (fn () =>
"Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
in
- if exists_type ResAxioms.type_has_empty_sort (prop_of st0)
+ if exists_type Res_Axioms.type_has_empty_sort (prop_of st0)
then (warning "Proof state contains the empty sort"; Seq.empty)
else
- (Meson.MESON ResAxioms.neg_clausify
+ (Meson.MESON Res_Axioms.neg_clausify
(fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i
- THEN ResAxioms.expand_defs_tac st0) st0
+ THEN Res_Axioms.expand_defs_tac st0) st0
end
handle METIS s => (warning ("Metis: " ^ s); Seq.empty);
@@ -737,7 +737,7 @@
method @{binding metisF} FO "METIS for FOL problems" #>
method @{binding metisFT} FT "METIS With-fully typed translation" #>
Method.setup @{binding finish_clausify}
- (Scan.succeed (K (SIMPLE_METHOD (ResAxioms.expand_defs_tac refl))))
+ (Scan.succeed (K (SIMPLE_METHOD (Res_Axioms.expand_defs_tac refl))))
"cleanup after conversion to clauses";
end;
--- a/src/HOL/Tools/res_atp.ML Thu Oct 29 16:34:44 2009 +0100
+++ b/src/HOL/Tools/res_atp.ML Thu Oct 29 16:59:12 2009 +0100
@@ -11,14 +11,14 @@
val get_relevant : int -> bool -> Proof.context * (thm list * 'a) -> thm list ->
(thm * (string * int)) list
val prepare_clauses : bool -> thm list -> thm list ->
- (thm * (ResHolClause.axiom_name * ResHolClause.clause_id)) list ->
- (thm * (ResHolClause.axiom_name * ResHolClause.clause_id)) list -> theory ->
- ResHolClause.axiom_name vector *
- (ResHolClause.clause list * ResHolClause.clause list * ResHolClause.clause list *
- ResHolClause.clause list * ResClause.classrelClause list * ResClause.arityClause list)
+ (thm * (Res_HOL_Clause.axiom_name * Res_HOL_Clause.clause_id)) list ->
+ (thm * (Res_HOL_Clause.axiom_name * Res_HOL_Clause.clause_id)) list -> theory ->
+ Res_HOL_Clause.axiom_name vector *
+ (Res_HOL_Clause.clause list * Res_HOL_Clause.clause list * Res_HOL_Clause.clause list *
+ Res_HOL_Clause.clause list * Res_Clause.classrelClause list * Res_Clause.arityClause list)
end;
-structure ResAtp: RES_ATP =
+structure Res_ATP: RES_ATP =
struct
@@ -238,10 +238,10 @@
let val cls = sort compare_pairs newpairs
val accepted = List.take (cls, max_new)
in
- ResAxioms.trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^
+ Res_Axioms.trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^
", exceeds the limit of " ^ Int.toString (max_new)));
- ResAxioms.trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
- ResAxioms.trace_msg (fn () => "Actually passed: " ^
+ Res_Axioms.trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
+ Res_Axioms.trace_msg (fn () => "Actually passed: " ^
space_implode ", " (map (fn (((_,(name,_)),_),_) => name) accepted));
(map #1 accepted, map #1 (List.drop (cls, max_new)))
@@ -256,7 +256,7 @@
val rel_consts' = List.foldl add_const_typ_table rel_consts new_consts
val newp = p + (1.0-p) / convergence
in
- ResAxioms.trace_msg (fn () => ("relevant this iteration: " ^ Int.toString (length newrels)));
+ Res_Axioms.trace_msg (fn () => "relevant this iteration: " ^ Int.toString (length newrels));
(map #1 newrels) @
(relevant_clauses max_new thy ctab newp rel_consts' (more_rejects@rejects))
end
@@ -264,12 +264,12 @@
let val weight = clause_weight ctab rel_consts consts_typs
in
if p <= weight orelse (follow_defs andalso defines thy (#1 clsthm) rel_consts)
- then (ResAxioms.trace_msg (fn () => (name ^ " clause " ^ Int.toString n ^
+ then (Res_Axioms.trace_msg (fn () => (name ^ " clause " ^ Int.toString n ^
" passes: " ^ Real.toString weight));
relevant ((ax,weight)::newrels, rejects) axs)
else relevant (newrels, ax::rejects) axs
end
- in ResAxioms.trace_msg (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p));
+ in Res_Axioms.trace_msg (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p));
relevant ([],[])
end;
@@ -278,12 +278,12 @@
then
let val const_tab = List.foldl (count_axiom_consts theory_const thy) Symtab.empty axioms
val goal_const_tab = get_goal_consts_typs thy goals
- val _ = ResAxioms.trace_msg (fn () => ("Initial constants: " ^
+ val _ = Res_Axioms.trace_msg (fn () => ("Initial constants: " ^
space_implode ", " (Symtab.keys goal_const_tab)));
val rels = relevant_clauses max_new thy const_tab (pass_mark)
goal_const_tab (map (pair_consts_typs_axiom theory_const thy) axioms)
in
- ResAxioms.trace_msg (fn () => ("Total relevant: " ^ Int.toString (length rels)));
+ Res_Axioms.trace_msg (fn () => ("Total relevant: " ^ Int.toString (length rels)));
rels
end
else axioms;
@@ -337,7 +337,7 @@
fun make_unique xs =
let val ht = mk_clause_table 7000
in
- ResAxioms.trace_msg (fn () => ("make_unique gets " ^ Int.toString (length xs) ^ " clauses"));
+ Res_Axioms.trace_msg (fn () => ("make_unique gets " ^ Int.toString (length xs) ^ " clauses"));
app (ignore o Polyhash.peekInsert ht) xs;
Polyhash.listItems ht
end;
@@ -359,7 +359,7 @@
else
let val xname = Facts.extern facts name in
if Name_Space.is_hidden xname then I
- else cons (xname, filter_out ResAxioms.bad_for_atp ths)
+ else cons (xname, filter_out Res_Axioms.bad_for_atp ths)
end) facts [];
fun all_valid_thms ctxt =
@@ -377,7 +377,7 @@
(*Ignore blacklisted basenames*)
fun add_multi_names (a, ths) pairs =
- if (Long_Name.base_name a) mem_string ResAxioms.multi_base_blacklist then pairs
+ if (Long_Name.base_name a) mem_string Res_Axioms.multi_base_blacklist then pairs
else add_single_names (a, ths) pairs;
fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
@@ -387,7 +387,7 @@
let
val (mults, singles) = List.partition is_multi (all_valid_thms ctxt)
fun blacklisted (_, th) =
- run_blacklist_filter andalso ResBlacklist.blacklisted ctxt th
+ run_blacklist_filter andalso Res_Blacklist.blacklisted ctxt th
in
filter_out blacklisted
(fold add_single_names singles (fold add_multi_names mults []))
@@ -399,7 +399,7 @@
fun get_all_lemmas ctxt =
let val included_thms =
- tap (fn ths => ResAxioms.trace_msg
+ tap (fn ths => Res_Axioms.trace_msg
(fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
(name_thm_pairs ctxt)
in
@@ -507,7 +507,7 @@
val thy = ProofContext.theory_of ctxt
val isFO = isFO thy goal_cls
val included_cls = get_all_lemmas ctxt
- |> ResAxioms.cnf_rules_pairs thy |> make_unique
+ |> Res_Axioms.cnf_rules_pairs thy |> make_unique
|> restrict_to_logic thy isFO
|> remove_unwanted_clauses
in
@@ -520,24 +520,24 @@
let
(* add chain thms *)
val chain_cls =
- ResAxioms.cnf_rules_pairs thy (filter check_named (map ResAxioms.pairname chain_ths))
+ Res_Axioms.cnf_rules_pairs thy (filter check_named (map Res_Axioms.pairname chain_ths))
val axcls = chain_cls @ axcls
val extra_cls = chain_cls @ extra_cls
val isFO = isFO thy goal_cls
val ccls = subtract_cls goal_cls extra_cls
- val _ = app (fn th => ResAxioms.trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
+ val _ = app (fn th => Res_Axioms.trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
val ccltms = map prop_of ccls
and axtms = map (prop_of o #1) extra_cls
val subs = tfree_classes_of_terms ccltms
and supers = tvar_classes_of_terms axtms
and tycons = type_consts_of_terms thy (ccltms@axtms)
(*TFrees in conjecture clauses; TVars in axiom clauses*)
- val conjectures = ResHolClause.make_conjecture_clauses dfg thy ccls
- val (_, extra_clauses) = ListPair.unzip (ResHolClause.make_axiom_clauses dfg thy extra_cls)
- val (clnames,axiom_clauses) = ListPair.unzip (ResHolClause.make_axiom_clauses dfg thy axcls)
- val helper_clauses = ResHolClause.get_helper_clauses dfg thy isFO (conjectures, extra_cls, [])
- val (supers',arity_clauses) = ResClause.make_arity_clauses_dfg dfg thy tycons supers
- val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
+ val conjectures = Res_HOL_Clause.make_conjecture_clauses dfg thy ccls
+ val (_, extra_clauses) = ListPair.unzip (Res_HOL_Clause.make_axiom_clauses dfg thy extra_cls)
+ val (clnames,axiom_clauses) = ListPair.unzip (Res_HOL_Clause.make_axiom_clauses dfg thy axcls)
+ val helper_clauses = Res_HOL_Clause.get_helper_clauses dfg thy isFO (conjectures, extra_cls, [])
+ val (supers',arity_clauses) = Res_Clause.make_arity_clauses_dfg dfg thy tycons supers
+ val classrel_clauses = Res_Clause.make_classrel_clauses thy subs supers'
in
(Vector.fromList clnames,
(conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses))
--- a/src/HOL/Tools/res_axioms.ML Thu Oct 29 16:34:44 2009 +0100
+++ b/src/HOL/Tools/res_axioms.ML Thu Oct 29 16:59:12 2009 +0100
@@ -23,7 +23,7 @@
val setup: theory -> theory
end;
-structure ResAxioms: RES_AXIOMS =
+structure Res_Axioms: RES_AXIOMS =
struct
val trace = Unsynchronized.ref false;
@@ -286,7 +286,7 @@
map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns s th);
-(*** Blacklisting (duplicated in ResAtp?) ***)
+(*** Blacklisting (duplicated in Res_ATP?) ***)
val max_lambda_nesting = 3;
@@ -387,14 +387,14 @@
fun cnf_rules_pairs_aux _ pairs [] = pairs
| cnf_rules_pairs_aux thy pairs ((name,th)::ths) =
let val pairs' = (pair_name_cls 0 (name, cnf_axiom thy th)) @ pairs
- handle THM _ => pairs | ResClause.CLAUSE _ => pairs
+ handle THM _ => pairs | Res_Clause.CLAUSE _ => pairs
in cnf_rules_pairs_aux thy pairs' ths end;
(*The combination of rev and tail recursion preserves the original order*)
fun cnf_rules_pairs thy l = cnf_rules_pairs_aux thy [] (rev l);
-(**** Convert all facts of the theory into clauses (ResClause.clause, or ResHolClause.clause) ****)
+(**** Convert all facts of the theory into clauses (Res_Clause.clause, or Res_HOL_Clause.clause) ****)
local
--- a/src/HOL/Tools/res_blacklist.ML Thu Oct 29 16:34:44 2009 +0100
+++ b/src/HOL/Tools/res_blacklist.ML Thu Oct 29 16:59:12 2009 +0100
@@ -16,7 +16,7 @@
val del: attribute
end;
-structure ResBlacklist: RES_BLACKLIST =
+structure Res_Blacklist: RES_BLACKLIST =
struct
structure Data = GenericDataFun
--- a/src/HOL/Tools/res_clause.ML Thu Oct 29 16:34:44 2009 +0100
+++ b/src/HOL/Tools/res_clause.ML Thu Oct 29 16:59:12 2009 +0100
@@ -77,7 +77,7 @@
val tptp_classrelClause : classrelClause -> string
end
-structure ResClause: RES_CLAUSE =
+structure Res_Clause: RES_CLAUSE =
struct
val schematic_var_prefix = "V_";
--- a/src/HOL/Tools/res_hol_clause.ML Thu Oct 29 16:34:44 2009 +0100
+++ b/src/HOL/Tools/res_hol_clause.ML Thu Oct 29 16:59:12 2009 +0100
@@ -17,13 +17,13 @@
type polarity = bool
type clause_id = int
datatype combterm =
- CombConst of string * ResClause.fol_type * ResClause.fol_type list (*Const and Free*)
- | CombVar of string * ResClause.fol_type
+ CombConst of string * Res_Clause.fol_type * Res_Clause.fol_type list (*Const and Free*)
+ | CombVar of string * Res_Clause.fol_type
| CombApp of combterm * combterm
datatype literal = Literal of polarity * combterm
datatype clause = Clause of {clause_id: clause_id, axiom_name: axiom_name, th: thm,
- kind: ResClause.kind,literals: literal list, ctypes_sorts: typ list}
- val type_of_combterm: combterm -> ResClause.fol_type
+ kind: Res_Clause.kind,literals: literal list, ctypes_sorts: typ list}
+ val type_of_combterm: combterm -> Res_Clause.fol_type
val strip_comb: combterm -> combterm * combterm list
val literals_of_term: theory -> term -> literal list * typ list
exception TOO_TRIVIAL
@@ -38,18 +38,18 @@
clause list
val tptp_write_file: bool -> Path.T ->
clause list * clause list * clause list * clause list *
- ResClause.classrelClause list * ResClause.arityClause list ->
+ Res_Clause.classrelClause list * Res_Clause.arityClause list ->
int * int
val dfg_write_file: bool -> Path.T ->
clause list * clause list * clause list * clause list *
- ResClause.classrelClause list * ResClause.arityClause list ->
+ Res_Clause.classrelClause list * Res_Clause.arityClause list ->
int * int
end
-structure ResHolClause: RES_HOL_CLAUSE =
+structure Res_HOL_Clause: RES_HOL_CLAUSE =
struct
-structure RC = ResClause;
+structure RC = Res_Clause; (* FIXME avoid structure alias *)
(* theorems for combinators and function extensionality *)
val ext = thm "HOL.ext";
@@ -404,7 +404,7 @@
else ct;
fun cnf_helper_thms thy =
- ResAxioms.cnf_rules_pairs thy o map ResAxioms.pairname
+ Res_Axioms.cnf_rules_pairs thy o map Res_Axioms.pairname
fun get_helper_clauses dfg thy isFO (conjectures, axcls, user_lemmas) =
if isFO then [] (*first-order*)
@@ -454,7 +454,7 @@
fold count_constants_lit literals (const_min_arity, const_needs_hBOOL);
fun display_arity const_needs_hBOOL (c,n) =
- ResAxioms.trace_msg (fn () => "Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^
+ Res_Axioms.trace_msg (fn () => "Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^
(if needs_hBOOL const_needs_hBOOL c then " needs hBOOL" else ""));
fun count_constants (conjectures, _, extra_clauses, helper_clauses, _, _) =
--- a/src/HOL/Tools/res_reconstruct.ML Thu Oct 29 16:34:44 2009 +0100
+++ b/src/HOL/Tools/res_reconstruct.ML Thu Oct 29 16:59:12 2009 +0100
@@ -24,13 +24,13 @@
string * string vector * (int * int) * Proof.context * thm * int -> string * string list
end;
-structure ResReconstruct : RES_RECONSTRUCT =
+structure Res_Reconstruct : RES_RECONSTRUCT =
struct
val trace_path = Path.basic "atp_trace";
fun trace s =
- if ! ResAxioms.trace then File.append (File.tmp_path trace_path) s
+ if ! Res_Axioms.trace then File.append (File.tmp_path trace_path) s
else ();
fun string_of_thm ctxt = PrintMode.setmp [] (Display.string_of_thm ctxt);
@@ -107,12 +107,12 @@
(*If string s has the prefix s1, return the result of deleting it.*)
fun strip_prefix s1 s =
if String.isPrefix s1 s
- then SOME (ResClause.undo_ascii_of (String.extract (s, size s1, NONE)))
+ then SOME (Res_Clause.undo_ascii_of (String.extract (s, size s1, NONE)))
else NONE;
(*Invert the table of translations between Isabelle and ATPs*)
val type_const_trans_table_inv =
- Symtab.make (map swap (Symtab.dest ResClause.type_const_trans_table));
+ Symtab.make (map swap (Symtab.dest Res_Clause.type_const_trans_table));
fun invert_type_const c =
case Symtab.lookup type_const_trans_table_inv c of
@@ -130,15 +130,15 @@
| Br (a,ts) =>
let val Ts = map type_of_stree ts
in
- case strip_prefix ResClause.tconst_prefix a of
+ case strip_prefix Res_Clause.tconst_prefix a of
SOME b => Type(invert_type_const b, Ts)
| NONE =>
if not (null ts) then raise STREE t (*only tconsts have type arguments*)
else
- case strip_prefix ResClause.tfree_prefix a of
+ case strip_prefix Res_Clause.tfree_prefix a of
SOME b => TFree("'" ^ b, HOLogic.typeS)
| NONE =>
- case strip_prefix ResClause.tvar_prefix a of
+ case strip_prefix Res_Clause.tvar_prefix a of
SOME b => make_tvar b
| NONE => make_tvar a (*Variable from the ATP, say X1*)
end;
@@ -146,7 +146,7 @@
(*Invert the table of translations between Isabelle and ATPs*)
val const_trans_table_inv =
Symtab.update ("fequal", "op =")
- (Symtab.make (map swap (Symtab.dest ResClause.const_trans_table)));
+ (Symtab.make (map swap (Symtab.dest Res_Clause.const_trans_table)));
fun invert_const c =
case Symtab.lookup const_trans_table_inv c of
@@ -167,7 +167,7 @@
| Br ("hBOOL",[t]) => term_of_stree [] thy t (*ignore hBOOL*)
| Br ("hAPP",[t,u]) => term_of_stree (u::args) thy t
| Br (a,ts) =>
- case strip_prefix ResClause.const_prefix a of
+ case strip_prefix Res_Clause.const_prefix a of
SOME "equal" =>
list_comb(Const ("op =", HOLogic.typeT), List.map (term_of_stree [] thy) ts)
| SOME b =>
@@ -181,10 +181,10 @@
| NONE => (*a variable, not a constant*)
let val T = HOLogic.typeT
val opr = (*a Free variable is typically a Skolem function*)
- case strip_prefix ResClause.fixed_var_prefix a of
+ case strip_prefix Res_Clause.fixed_var_prefix a of
SOME b => Free(b,T)
| NONE =>
- case strip_prefix ResClause.schematic_var_prefix a of
+ case strip_prefix Res_Clause.schematic_var_prefix a of
SOME b => make_var (b,T)
| NONE => make_var (a,T) (*Variable from the ATP, say X1*)
in list_comb (opr, List.map (term_of_stree [] thy) (ts@args)) end;
@@ -194,7 +194,7 @@
| constraint_of_stree pol t = case t of
Int _ => raise STREE t
| Br (a,ts) =>
- (case (strip_prefix ResClause.class_prefix a, map type_of_stree ts) of
+ (case (strip_prefix Res_Clause.class_prefix a, map type_of_stree ts) of
(SOME b, [T]) => (pol, b, T)
| _ => raise STREE t);
@@ -444,11 +444,11 @@
val _ = trace (Int.toString (length nonnull_lines) ^ " nonnull_lines extracted\n")
val (_,lines) = List.foldr (add_wanted_prfline ctxt) (0,[]) nonnull_lines
val _ = trace (Int.toString (length lines) ^ " lines extracted\n")
- val (ccls,fixes) = ResAxioms.neg_conjecture_clauses ctxt th sgno
+ val (ccls,fixes) = Res_Axioms.neg_conjecture_clauses ctxt th sgno
val _ = trace (Int.toString (length ccls) ^ " conjecture clauses\n")
val ccls = map forall_intr_vars ccls
val _ =
- if ! ResAxioms.trace then app (fn th => trace ("\nccl: " ^ string_of_thm ctxt th)) ccls
+ if ! Res_Axioms.trace then app (fn th => trace ("\nccl: " ^ string_of_thm ctxt th)) ccls
else ()
val ilines = isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines)
val _ = trace "\ndecode_tstp_file: finishing\n"