--- 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
--- 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
--- 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
--- 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 \<Longrightarrow> length ys = length vs \<Longrightarrow> map (the \<circ> f(ys[\<mapsto>]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
--- 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;
--- 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;
--- 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
--- 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" **)