# HG changeset patch # User blanchet # Date 1285798331 -7200 # Node ID 699a20afc5bd54ca69dffb9a05135d4f1a3595ee # Parent 8e12f1956fcd615d2f538ff2b37e97045248af55 Skolemizer tweaking diff -r 8e12f1956fcd -r 699a20afc5bd src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Wed Sep 29 23:55:14 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Sep 30 00:12:11 2010 +0200 @@ -84,7 +84,7 @@ else tp :: map (apsnd (subst_atomic [tp])) inst fun is_flex t = case strip_comb t of - (Var _, args) => forall (is_Bound orf is_Var orf is_Free) args + (Var _, args) => forall (is_Bound orf is_Var (*FIXME: orf is_Free*)) args | _ => false fun unify_flex flex rigid = case strip_comb flex of @@ -111,7 +111,11 @@ fun unify_prem prem = let val inst = [] |> unify_terms (prem, concl) - val instT = fold (unify_types o pairself fastype_of) inst [] + val _ = trace_msg (fn () => cat_lines (map (fn (t, u) => + Syntax.string_of_term @{context} t ^ " |-> " ^ + Syntax.string_of_term @{context} u) inst)) + val instT = fold (fn Tp => unify_types (pairself fastype_of Tp) + handle TERM _ => I) inst [] val inst = inst |> map (pairself (subst_atomic_types instT)) val cinstT = instT |> map (pairself (ctyp_of thy)) val cinst = inst |> map (pairself (cterm_of thy)) @@ -138,7 +142,8 @@ Goal.prove ctxt [] [] @{prop False} (K (cut_rules_tac axioms 1 THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1) -(* FIXME: THEN etac @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast} 1 *) + (* two copies are better than one (FIXME) *) + THEN etac @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast} 1 THEN TRY (REPEAT_ALL_NEW (etac @{thm allE}) 1) THEN match_tac [premises_imp_false] 1 THEN DETERM_UNTIL_SOLVED