# HG changeset patch # User huffman # Date 1286806182 25200 # Node ID a4b2971952f46898ca0b800685d575378da0a447 # Parent 8c2f449af35a52237f2cd3df662807bfe87c2422# Parent f175e482dabebdc3d7a606d56c9d35afbf29e087 merged diff -r 8c2f449af35a -r a4b2971952f4 doc-src/IsarRef/Thy/Spec.thy --- a/doc-src/IsarRef/Thy/Spec.thy Sat Oct 09 07:24:49 2010 -0700 +++ b/doc-src/IsarRef/Thy/Spec.thy Mon Oct 11 07:09:42 2010 -0700 @@ -1209,8 +1209,7 @@ \item @{command "hide_class"}~@{text names} fully removes class declarations from a given name space; with the @{text "(open)"} - option, only the base name is hidden. Global (unqualified) names - may never be hidden. + option, only the base name is hidden. Note that hiding name space accesses has no impact on logical declarations --- they remain valid internally. Entities that are no diff -r 8c2f449af35a -r a4b2971952f4 doc-src/IsarRef/Thy/document/Spec.tex --- a/doc-src/IsarRef/Thy/document/Spec.tex Sat Oct 09 07:24:49 2010 -0700 +++ b/doc-src/IsarRef/Thy/document/Spec.tex Mon Oct 11 07:09:42 2010 -0700 @@ -1252,8 +1252,7 @@ \item \hyperlink{command.hide-class}{\mbox{\isa{\isacommand{hide{\isacharunderscore}class}}}}~\isa{names} fully removes class declarations from a given name space; with the \isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}} - option, only the base name is hidden. Global (unqualified) names - may never be hidden. + option, only the base name is hidden. Note that hiding name space accesses has no impact on logical declarations --- they remain valid internally. Entities that are no diff -r 8c2f449af35a -r a4b2971952f4 src/HOL/Metis.thy --- a/src/HOL/Metis.thy Sat Oct 09 07:24:49 2010 -0700 +++ b/src/HOL/Metis.thy Mon Oct 11 07:09:42 2010 -0700 @@ -29,7 +29,11 @@ use "Tools/Metis/metis_translate.ML" use "Tools/Metis/metis_reconstruct.ML" use "Tools/Metis/metis_tactics.ML" -setup Metis_Tactics.setup + +setup {* + Metis_Reconstruct.setup + #> Metis_Tactics.setup +*} hide_const (open) fequal hide_fact (open) fequal_def fequal_imp_equal equal_imp_fequal equal_imp_equal diff -r 8c2f449af35a -r a4b2971952f4 src/HOL/MicroJava/Comp/AuxLemmas.thy --- a/src/HOL/MicroJava/Comp/AuxLemmas.thy Sat Oct 09 07:24:49 2010 -0700 +++ b/src/HOL/MicroJava/Comp/AuxLemmas.thy Mon Oct 11 07:09:42 2010 -0700 @@ -86,7 +86,7 @@ lemma map_upds_distinct [simp]: "distinct ys \ length ys = length vs \ map (the \ f(ys[\]vs)) ys = vs" -apply (induct ys arbitrary: f vs rule: distinct.induct) +apply (induct ys arbitrary: f vs) apply simp apply (case_tac vs) apply simp_all diff -r 8c2f449af35a -r a4b2971952f4 src/HOL/Tools/Meson/meson.ML --- a/src/HOL/Tools/Meson/meson.ML Sat Oct 09 07:24:49 2010 -0700 +++ b/src/HOL/Tools/Meson/meson.ML Mon Oct 11 07:09:42 2010 -0700 @@ -8,7 +8,8 @@ signature MESON = sig - val trace: bool Unsynchronized.ref + val trace : bool Config.T + val max_clauses : int Config.T val term_pair_of: indexname * (typ * 'a) -> term * 'a val size_of_subgoals: thm -> int val has_too_many_clauses: Proof.context -> term -> bool @@ -39,17 +40,19 @@ val make_meta_clause: thm -> thm val make_meta_clauses: thm list -> thm list val meson_tac: Proof.context -> thm list -> int -> tactic - val setup: theory -> theory + val setup : theory -> theory end structure Meson : MESON = struct -val trace = Unsynchronized.ref false; -fun trace_msg msg = if ! trace then tracing (msg ()) else (); +val (trace, trace_setup) = Attrib.config_bool "trace_meson" (K false) + +fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else () -val max_clauses_default = 60; -val (max_clauses, setup) = Attrib.config_int "meson_max_clauses" (K max_clauses_default); +val max_clauses_default = 60 +val (max_clauses, max_clauses_setup) = + Attrib.config_int "meson_max_clauses" (K max_clauses_default) (*No known example (on 1-5-2007) needs even thirty*) val iter_deepen_limit = 50; @@ -366,7 +369,7 @@ and cnf_nil th = cnf_aux (th,[]) val cls = if has_too_many_clauses ctxt (concl_of th) - then (trace_msg (fn () => "cnf is ignoring: " ^ Display.string_of_thm ctxt th); ths) + then (trace_msg ctxt (fn () => "cnf is ignoring: " ^ Display.string_of_thm ctxt th); ths) else cnf_aux (th,ths) in (cls, !ctxtr) end; @@ -586,8 +589,8 @@ (* "RS" can fail if "unify_search_bound" is too small. *) fun try_skolemize ctxt th = try (skolemize ctxt) th - |> tap (fn NONE => trace_msg (fn () => "Failed to skolemize " ^ - Display.string_of_thm ctxt th) + |> tap (fn NONE => trace_msg ctxt (fn () => "Failed to skolemize " ^ + Display.string_of_thm ctxt th) | _ => ()) fun add_clauses th cls = @@ -678,7 +681,7 @@ | goes => let val horns = make_horns (cls @ ths) - val _ = trace_msg (fn () => + val _ = trace_msg ctxt (fn () => cat_lines ("meson method called:" :: map (Display.string_of_thm ctxt) (cls @ ths) @ ["clauses:"] @ map (Display.string_of_thm ctxt) horns)) @@ -717,4 +720,8 @@ name_thms "MClause#" (distinct Thm.eq_thm_prop (map make_meta_clause ths)); +val setup = + trace_setup + #> max_clauses_setup + end; diff -r 8c2f449af35a -r a4b2971952f4 src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Sat Oct 09 07:24:49 2010 -0700 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Mon Oct 11 07:09:42 2010 -0700 @@ -11,7 +11,8 @@ sig type mode = Metis_Translate.mode - val trace : bool Unsynchronized.ref + val trace : bool Config.T + val trace_msg : Proof.context -> (unit -> string) -> unit val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a val untyped_aconv : term -> term -> bool val replay_one_inference : @@ -20,6 +21,7 @@ -> (Metis_Thm.thm * thm) list val discharge_skolem_premises : Proof.context -> (thm * term) option list -> thm -> thm + val setup : theory -> theory end; structure Metis_Reconstruct : METIS_RECONSTRUCT = @@ -27,8 +29,9 @@ open Metis_Translate -val trace = Unsynchronized.ref false -fun trace_msg msg = if !trace then tracing (msg ()) else () +val (trace, trace_setup) = Attrib.config_bool "trace_metis" (K false) + +fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else () datatype term_or_type = SomeTerm of term | SomeType of typ @@ -92,8 +95,8 @@ (*Maps metis terms to isabelle terms*) fun hol_term_from_metis_PT ctxt fol_tm = let val thy = ProofContext.theory_of ctxt - val _ = trace_msg (fn () => "hol_term_from_metis_PT: " ^ - Metis_Term.toString fol_tm) + val _ = trace_msg ctxt (fn () => "hol_term_from_metis_PT: " ^ + Metis_Term.toString fol_tm) fun tm_to_tt (Metis_Term.Var v) = (case strip_prefix_and_unascii tvar_prefix v of SOME w => SomeType (make_tvar w) @@ -160,8 +163,8 @@ (*Maps fully-typed metis terms to isabelle terms*) fun hol_term_from_metis_FT ctxt fol_tm = - let val _ = trace_msg (fn () => "hol_term_from_metis_FT: " ^ - Metis_Term.toString fol_tm) + let val _ = trace_msg ctxt (fn () => "hol_term_from_metis_FT: " ^ + Metis_Term.toString fol_tm) fun cvt (Metis_Term.Fn ("ti", [Metis_Term.Var v, _])) = (case strip_prefix_and_unascii schematic_var_prefix v of SOME w => mk_var(w, dummyT) @@ -188,10 +191,12 @@ | NONE => (*Not a constant. Is it a fixed variable??*) case strip_prefix_and_unascii fixed_var_prefix x of SOME v => Free (v, dummyT) - | NONE => (trace_msg (fn () => "hol_term_from_metis_FT bad const: " ^ x); - hol_term_from_metis_PT ctxt t)) - | cvt t = (trace_msg (fn () => "hol_term_from_metis_FT bad term: " ^ Metis_Term.toString t); - hol_term_from_metis_PT ctxt t) + | NONE => (trace_msg ctxt (fn () => + "hol_term_from_metis_FT bad const: " ^ x); + hol_term_from_metis_PT ctxt t)) + | cvt t = (trace_msg ctxt (fn () => + "hol_term_from_metis_FT bad term: " ^ Metis_Term.toString t); + hol_term_from_metis_PT ctxt t) in fol_tm |> cvt end fun hol_term_from_metis FT = hol_term_from_metis_FT @@ -199,11 +204,12 @@ fun hol_terms_from_fol ctxt mode old_skolems fol_tms = let val ts = map (hol_term_from_metis mode ctxt) fol_tms - val _ = trace_msg (fn () => " calling type inference:") - val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts + val _ = trace_msg ctxt (fn () => " calling type inference:") + val _ = app (fn t => trace_msg ctxt + (fn () => Syntax.string_of_term ctxt t)) ts val ts' = ts |> map (reveal_old_skolem_terms old_skolems) |> infer_types ctxt - val _ = app (fn t => trace_msg + val _ = app (fn t => trace_msg ctxt (fn () => " final term: " ^ Syntax.string_of_term ctxt t ^ " of type " ^ Syntax.string_of_typ ctxt (type_of t))) ts' @@ -215,10 +221,10 @@ (*for debugging only*) (* -fun print_thpair (fth,th) = - (trace_msg (fn () => "============================================="); - trace_msg (fn () => "Metis: " ^ Metis_Thm.toString fth); - trace_msg (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th)); +fun print_thpair ctxt (fth,th) = + (trace_msg ctxt (fn () => "============================================="); + trace_msg ctxt (fn () => "Metis: " ^ Metis_Thm.toString fth); + trace_msg ctxt (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th)); *) fun lookth thpairs (fth : Metis_Thm.thm) = @@ -264,12 +270,12 @@ val t = hol_term_from_metis mode ctxt y in SOME (cterm_of thy (Var v), t) end handle Option.Option => - (trace_msg (fn () => "\"find_var\" failed for " ^ x ^ - " in " ^ Display.string_of_thm ctxt i_th); + (trace_msg ctxt (fn () => "\"find_var\" failed for " ^ x ^ + " in " ^ Display.string_of_thm ctxt i_th); NONE) | TYPE _ => - (trace_msg (fn () => "\"hol_term_from_metis\" failed for " ^ x ^ - " in " ^ Display.string_of_thm ctxt i_th); + (trace_msg ctxt (fn () => "\"hol_term_from_metis\" failed for " ^ x ^ + " in " ^ Display.string_of_thm ctxt i_th); NONE) fun remove_typeinst (a, t) = case strip_prefix_and_unascii schematic_var_prefix a of @@ -277,14 +283,14 @@ | NONE => case strip_prefix_and_unascii 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) + val _ = trace_msg ctxt (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th) val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst) val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs) val tms = rawtms |> map (reveal_old_skolem_terms old_skolems) |> infer_types ctxt val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th) val substs' = ListPair.zip (vars, map ctm_of tms) - val _ = trace_msg (fn () => + val _ = trace_msg ctxt (fn () => cat_lines ("subst_translations:" :: (substs' |> map (fn (x, y) => Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^ @@ -375,8 +381,8 @@ let val thy = ProofContext.theory_of ctxt val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2 - val _ = trace_msg (fn () => " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1) - val _ = trace_msg (fn () => " isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2) + val _ = trace_msg ctxt (fn () => " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1) + val _ = trace_msg ctxt (fn () => " isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2) in (* Trivial cases where one operand is type info *) if Thm.eq_thm (TrueI, i_th1) then @@ -387,15 +393,15 @@ let val i_atm = singleton (hol_terms_from_fol ctxt mode old_skolems) (Metis_Term.Fn atm) - val _ = trace_msg (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atm) + val _ = trace_msg ctxt (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atm) val prems_th1 = prems_of i_th1 val prems_th2 = prems_of i_th2 val index_th1 = literal_index (mk_not i_atm) prems_th1 handle Empty => raise Fail "Failed to find literal in th1" - val _ = trace_msg (fn () => " index_th1: " ^ Int.toString index_th1) + val _ = trace_msg ctxt (fn () => " index_th1: " ^ Int.toString index_th1) val index_th2 = literal_index i_atm prems_th2 handle Empty => raise Fail "Failed to find literal in th2" - val _ = trace_msg (fn () => " index_th2: " ^ Int.toString index_th2) + val _ = trace_msg ctxt (fn () => " index_th2: " ^ Int.toString index_th2) in resolve_inc_tyvars thy (select_literal index_th1 i_th1) index_th2 i_th2 end @@ -411,7 +417,7 @@ fun refl_inf ctxt mode old_skolems t = let val thy = ProofContext.theory_of ctxt val i_t = singleton (hol_terms_from_fol ctxt mode old_skolems) t - val _ = trace_msg (fn () => " term: " ^ Syntax.string_of_term ctxt i_t) + val _ = trace_msg ctxt (fn () => " term: " ^ Syntax.string_of_term ctxt i_t) val c_t = cterm_incr_types thy refl_idx i_t in cterm_instantiate [(refl_x, c_t)] REFL_THM end; @@ -430,7 +436,7 @@ let val thy = ProofContext.theory_of ctxt val m_tm = Metis_Term.Fn atm val [i_atm,i_tm] = hol_terms_from_fol ctxt mode old_skolems [m_tm, fr] - val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos) + val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos) fun replace_item_list lx 0 (_::ls) = lx::ls | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls fun path_finder_FO tm [] = (tm, Bound 0) @@ -444,7 +450,7 @@ "equality_inf: " ^ Int.toString p ^ " adj " ^ Int.toString adjustment ^ " term " ^ Syntax.string_of_term ctxt tm) - val _ = trace_msg (fn () => "path_finder: " ^ Int.toString p ^ + val _ = trace_msg ctxt (fn () => "path_finder: " ^ Int.toString p ^ " " ^ Syntax.string_of_term ctxt tm_p) val (r,t) = path_finder_FO tm_p ps in @@ -496,12 +502,12 @@ | path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm val (tm_subst, body) = path_finder_lit i_atm fp val tm_abs = Abs ("x", type_of tm_subst, body) - val _ = trace_msg (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs) - val _ = trace_msg (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm) - val _ = trace_msg (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst) + val _ = trace_msg ctxt (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs) + val _ = trace_msg ctxt (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm) + val _ = trace_msg ctxt (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst) val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill typed but gives right max*) val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em) - val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst') + val _ = trace_msg ctxt (fn () => "subst' " ^ Display.string_of_thm ctxt subst') val eq_terms = map (pairself (cterm_of thy)) (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm])) in cterm_instantiate eq_terms subst' end; @@ -540,13 +546,13 @@ fun replay_one_inference ctxt mode old_skolems (fol_th, inf) thpairs = let - val _ = trace_msg (fn () => "=============================================") - val _ = trace_msg (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th) - val _ = trace_msg (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf) + val _ = trace_msg ctxt (fn () => "=============================================") + val _ = trace_msg ctxt (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th) + val _ = trace_msg ctxt (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf) val th = step ctxt mode old_skolems thpairs (fol_th, inf) |> flexflex_first_order - val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th) - val _ = trace_msg (fn () => "=============================================") + val _ = trace_msg ctxt (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th) + val _ = trace_msg ctxt (fn () => "=============================================") val num_metis_lits = fol_th |> Metis_Thm.clause |> Metis_LiteralSet.toList |> count is_metis_literal_genuine @@ -556,8 +562,6 @@ else error "Cannot replay Metis proof in Isabelle: Out of sync." in (fol_th, th) :: thpairs end -(* FIXME ### GET RID OF skolem WRAPPER by looking at substitution *) - fun term_instantiate thy = cterm_instantiate o map (pairself (cterm_of thy)) (* In principle, it should be sufficient to apply "assume_tac" to unify the @@ -790,8 +794,10 @@ THEN ALLGOALS (fn i => rtac @{thm Meson.skolem_COMBK_I} i THEN rotate_tac (rotation_for_subgoal i) i - THEN PRIMITIVE (unify_first_prem_with_concl thy i) +(* THEN PRIMITIVE (unify_first_prem_with_concl thy i) ###*) THEN assume_tac i))) end +val setup = trace_setup + end; diff -r 8c2f449af35a -r a4b2971952f4 src/HOL/Tools/Metis/metis_tactics.ML --- a/src/HOL/Tools/Metis/metis_tactics.ML Sat Oct 09 07:24:49 2010 -0700 +++ b/src/HOL/Tools/Metis/metis_tactics.ML Mon Oct 11 07:09:42 2010 -0700 @@ -9,7 +9,7 @@ signature METIS_TACTICS = sig - val trace : bool Unsynchronized.ref + val trace : bool Config.T val type_lits : bool Config.T val new_skolemizer : bool Config.T val metis_tac : Proof.context -> thm list -> int -> tactic @@ -24,8 +24,6 @@ open Metis_Translate open Metis_Reconstruct -fun trace_msg msg = if !trace then tracing (msg ()) else () - val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true) val (new_skolemizer, new_skolemizer_setup) = Attrib.config_bool "metis_new_skolemizer" (K false) @@ -67,21 +65,21 @@ (0 upto length ths0 - 1) ths0 val thss = map (snd o snd) th_cls_pairs val dischargers = map (fst o snd) 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 - val _ = trace_msg (fn () => "THEOREM CLAUSES") - val _ = app (app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th))) thss + val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") + val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls + val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES") + val _ = app (app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th))) thss val (mode, {axioms, tfrees, old_skolems}) = build_logic_map mode ctxt type_lits cls thss val _ = if null tfrees then () - else (trace_msg (fn () => "TFREE CLAUSES"); + else (trace_msg ctxt (fn () => "TFREE CLAUSES"); app (fn TyLitFree ((s, _), (s', _)) => - trace_msg (fn () => s ^ "(" ^ s' ^ ")")) tfrees) - val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS") + trace_msg ctxt (fn () => s ^ "(" ^ s' ^ ")")) tfrees) + val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS") val thms = map #1 axioms - val _ = app (fn th => trace_msg (fn () => Metis_Thm.toString th)) thms - val _ = trace_msg (fn () => "mode = " ^ string_of_mode mode) - val _ = trace_msg (fn () => "START METIS PROVE PROCESS") + val _ = app (fn th => trace_msg ctxt (fn () => Metis_Thm.toString th)) thms + val _ = trace_msg ctxt (fn () => "mode = " ^ string_of_mode mode) + val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS") in case filter (is_false o prop_of) cls of false_th::_ => [false_th RS @{thm FalseE}] @@ -89,7 +87,7 @@ case Metis_Resolution.new resolution_params {axioms = thms, conjecture = []} |> Metis_Resolution.loop of Metis_Resolution.Contradiction mth => - let val _ = trace_msg (fn () => "METIS RECONSTRUCTION START: " ^ + let val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^ Metis_Thm.toString mth) val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt (*add constraints arising from converting goal to clause form*) @@ -97,8 +95,8 @@ val result = fold (replay_one_inference ctxt' mode old_skolems) proof axioms and used = map_filter (used_axioms axioms) proof - val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:") - val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used + val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:") + val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used val unused = th_cls_pairs |> map_filter (fn (name, (_, cls)) => if have_common_thm used cls then NONE else SOME name) in @@ -113,12 +111,12 @@ (); case result of (_,ith)::_ => - (trace_msg (fn () => "Success: " ^ Display.string_of_thm ctxt ith); + (trace_msg ctxt (fn () => "Success: " ^ Display.string_of_thm ctxt ith); [discharge_skolem_premises ctxt dischargers ith]) - | _ => (trace_msg (fn () => "Metis: No result"); []) + | _ => (trace_msg ctxt (fn () => "Metis: No result"); []) end | Metis_Resolution.Satisfiable _ => - (trace_msg (fn () => "Metis: No first-order proof with the lemmas supplied"); + (trace_msg ctxt (fn () => "Metis: No first-order proof with the lemmas supplied"); []) end; @@ -150,7 +148,7 @@ fun generic_metis_tac mode ctxt ths i st0 = let - val _ = trace_msg (fn () => + val _ = trace_msg ctxt (fn () => "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths)) in if exists_type type_has_top_sort (prop_of st0) then diff -r 8c2f449af35a -r a4b2971952f4 src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Sat Oct 09 07:24:49 2010 -0700 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Mon Oct 11 07:09:42 2010 -0700 @@ -13,10 +13,6 @@ val axiom_prefix : string val conjecture_prefix : string - val helper_prefix : string - val class_rel_clause_prefix : string - val arity_clause_prefix : string - val tfrees_name : string val prepare_axiom : Proof.context -> (string * 'a) * thm -> term * ((string * 'a) * fol_formula) option @@ -38,7 +34,7 @@ val helper_prefix = "help_" val class_rel_clause_prefix = "clrel_"; val arity_clause_prefix = "arity_" -val tfrees_name = "tfrees" +val tfree_prefix = "tfree_" (* Freshness almost guaranteed! *) val sledgehammer_weak_prefix = "Sledgehammer:" @@ -363,13 +359,13 @@ fun free_type_literals_for_conjecture ({ctypes_sorts, ...} : fol_formula) = map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts) -fun problem_line_for_free_type lit = - Fof (tfrees_name, Hypothesis, formula_for_fo_literal lit) +fun problem_line_for_free_type j lit = + Fof (tfree_prefix ^ string_of_int j, Hypothesis, formula_for_fo_literal lit) fun problem_lines_for_free_types conjectures = let val litss = map free_type_literals_for_conjecture conjectures val lits = fold (union (op =)) litss [] - in map problem_line_for_free_type lits end + in map2 problem_line_for_free_type (0 upto length lits - 1) lits end (** "hBOOL" and "hAPP" **)