# HG changeset patch
# User blanchet
# Date 1314713063 -7200
# Node ID e74aa9d9162be071cb3a1bfc52e288dfad6a5e01
# Parent  0f50f158eb5741e5baa3c76928274cdbd4ccacb8
tuning

diff -r 0f50f158eb57 -r e74aa9d9162b src/HOL/Tools/Metis/metis_tactics.ML
--- a/src/HOL/Tools/Metis/metis_tactics.ML	Tue Aug 30 14:29:39 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML	Tue Aug 30 16:04:23 2011 +0200
@@ -89,12 +89,12 @@
   end
   |> Meson.make_meta_clause
 
-fun clause_params type_enc =
+val clause_params =
   {ordering = Metis_KnuthBendixOrder.default,
    orderLiterals = Metis_Clause.UnsignedLiteralOrder,
    orderTerms = true}
-fun active_params type_enc =
-  {clause = clause_params type_enc,
+val active_params =
+  {clause = clause_params,
    prefactor = #prefactor Metis_Active.default,
    postfactor = #postfactor Metis_Active.default}
 val waiting_params =
@@ -102,8 +102,7 @@
    variablesWeight = 0.0,
    literalsWeight = 0.0,
    models = []}
-fun resolution_params type_enc =
-  {active = active_params type_enc, waiting = waiting_params}
+val resolution_params = {active = active_params, waiting = waiting_params}
 
 (* Main function to start Metis proof and reconstruction *)
 fun FOL_SOLVE (type_enc :: fallback_type_syss) ctxt cls ths0 =
@@ -137,7 +136,7 @@
       case filter (fn t => prop_of t aconv @{prop False}) cls of
           false_th :: _ => [false_th RS @{thm FalseE}]
         | [] =>
-      case Metis_Resolution.new (resolution_params type_enc)
+      case Metis_Resolution.new resolution_params
                                 {axioms = thms, conjecture = []}
            |> Metis_Resolution.loop of
           Metis_Resolution.Contradiction mth =>