tuning
authorblanchet
Tue Aug 30 16:04:23 2011 +0200 (2011-08-30)
changeset 44588e74aa9d9162b
parent 44587 0f50f158eb57
child 44589 0a1dfc6365e9
tuning
src/HOL/Tools/Metis/metis_tactics.ML
     1.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML	Tue Aug 30 14:29:39 2011 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_tactics.ML	Tue Aug 30 16:04:23 2011 +0200
     1.3 @@ -89,12 +89,12 @@
     1.4    end
     1.5    |> Meson.make_meta_clause
     1.6  
     1.7 -fun clause_params type_enc =
     1.8 +val clause_params =
     1.9    {ordering = Metis_KnuthBendixOrder.default,
    1.10     orderLiterals = Metis_Clause.UnsignedLiteralOrder,
    1.11     orderTerms = true}
    1.12 -fun active_params type_enc =
    1.13 -  {clause = clause_params type_enc,
    1.14 +val active_params =
    1.15 +  {clause = clause_params,
    1.16     prefactor = #prefactor Metis_Active.default,
    1.17     postfactor = #postfactor Metis_Active.default}
    1.18  val waiting_params =
    1.19 @@ -102,8 +102,7 @@
    1.20     variablesWeight = 0.0,
    1.21     literalsWeight = 0.0,
    1.22     models = []}
    1.23 -fun resolution_params type_enc =
    1.24 -  {active = active_params type_enc, waiting = waiting_params}
    1.25 +val resolution_params = {active = active_params, waiting = waiting_params}
    1.26  
    1.27  (* Main function to start Metis proof and reconstruction *)
    1.28  fun FOL_SOLVE (type_enc :: fallback_type_syss) ctxt cls ths0 =
    1.29 @@ -137,7 +136,7 @@
    1.30        case filter (fn t => prop_of t aconv @{prop False}) cls of
    1.31            false_th :: _ => [false_th RS @{thm FalseE}]
    1.32          | [] =>
    1.33 -      case Metis_Resolution.new (resolution_params type_enc)
    1.34 +      case Metis_Resolution.new resolution_params
    1.35                                  {axioms = thms, conjecture = []}
    1.36             |> Metis_Resolution.loop of
    1.37            Metis_Resolution.Contradiction mth =>