removed pointless warning (cf. http://stackoverflow.com/questions/20233463/isabelle-metis-proof-state-contains-the-universal-sort/20785045#20785045)
authorblanchet
Thu Jan 02 19:07:36 2014 +0100 (2014-01-02 ago)
changeset 5491425212efcd0de
parent 54913 7b18c41df27a
child 54915 61284fe0536a
removed pointless warning (cf. http://stackoverflow.com/questions/20233463/isabelle-metis-proof-state-contains-the-universal-sort/20785045#20785045)
src/HOL/Tools/Metis/metis_tactic.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
     1.1 --- a/src/HOL/Tools/Metis/metis_tactic.ML	Thu Jan 02 09:50:22 2014 +0100
     1.2 +++ b/src/HOL/Tools/Metis/metis_tactic.ML	Thu Jan 02 19:07:36 2014 +0100
     1.3 @@ -13,7 +13,6 @@
     1.4    val verbose : bool Config.T
     1.5    val new_skolem : bool Config.T
     1.6    val advisory_simp : bool Config.T
     1.7 -  val type_has_top_sort : typ -> bool
     1.8    val metis_tac : string list -> string -> Proof.context -> thm list -> int -> tactic
     1.9    val metis_lam_transs : string list
    1.10    val parse_metis_options : (string list option * string option) parser
    1.11 @@ -250,9 +249,6 @@
    1.12     else
    1.13       all_tac) st0
    1.14  
    1.15 -val type_has_top_sort =
    1.16 -  exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
    1.17 -
    1.18  fun generic_metis_tac type_encs lam_trans ctxt ths i st0 =
    1.19    let
    1.20      val _ = trace_msg ctxt (fn () =>
    1.21 @@ -262,12 +258,7 @@
    1.22      fun tac clause =
    1.23        resolve_tac (FOL_SOLVE type_encs lam_trans ctxt clause ths) 1
    1.24    in
    1.25 -    if exists_type type_has_top_sort (prop_of st0) then
    1.26 -      verbose_warning ctxt "Proof state contains the universal sort {}"
    1.27 -    else
    1.28 -      ();
    1.29 -    Meson.MESON (preskolem_tac ctxt)
    1.30 -        (maps (neg_clausify ctxt (lam_trans = combsN))) tac ctxt i st0
    1.31 +    Meson.MESON (preskolem_tac ctxt) (maps (neg_clausify ctxt (lam_trans = combsN))) tac ctxt i st0
    1.32    end
    1.33  
    1.34  fun metis_tac [] = generic_metis_tac partial_type_encs
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Jan 02 09:50:22 2014 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Jan 02 19:07:36 2014 +0100
     2.3 @@ -246,6 +246,9 @@
     2.4    | combine_interests _ Interesting = Interesting
     2.5    | combine_interests Boring Boring = Boring
     2.6  
     2.7 +val type_has_top_sort =
     2.8 +  exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
     2.9 +
    2.10  fun is_likely_tautology_too_meta_or_too_technical th =
    2.11    let
    2.12      fun is_interesting_subterm (Const (s, _)) =