# HG changeset patch # User wenzelm # Date 1256831952 -3600 # Node ID 6a72af4e84b8e38650bb2e97a063e908867b565d # Parent 784c1b09d4851cbf08706eeb2ff1875f5f06edee modernized some structure names; diff -r 784c1b09d485 -r 6a72af4e84b8 src/HOL/ATP_Linkup.thy --- 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 diff -r 784c1b09d485 -r 6a72af4e84b8 src/HOL/HOL.thy --- 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 *} diff -r 784c1b09d485 -r 6a72af4e84b8 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- 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) diff -r 784c1b09d485 -r 6a72af4e84b8 src/HOL/Tools/ATP_Manager/atp_manager.ML --- 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 ()); diff -r 784c1b09d485 -r 6a72af4e84b8 src/HOL/Tools/ATP_Manager/atp_minimal.ML --- 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 diff -r 784c1b09d485 -r 6a72af4e84b8 src/HOL/Tools/ATP_Manager/atp_wrapper.ML --- 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 diff -r 784c1b09d485 -r 6a72af4e84b8 src/HOL/Tools/metis_tools.ML --- 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; diff -r 784c1b09d485 -r 6a72af4e84b8 src/HOL/Tools/res_atp.ML --- 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)) diff -r 784c1b09d485 -r 6a72af4e84b8 src/HOL/Tools/res_axioms.ML --- 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 diff -r 784c1b09d485 -r 6a72af4e84b8 src/HOL/Tools/res_blacklist.ML --- 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 diff -r 784c1b09d485 -r 6a72af4e84b8 src/HOL/Tools/res_clause.ML --- 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_"; diff -r 784c1b09d485 -r 6a72af4e84b8 src/HOL/Tools/res_hol_clause.ML --- 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, _, _) = diff -r 784c1b09d485 -r 6a72af4e84b8 src/HOL/Tools/res_reconstruct.ML --- 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"