--- 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 =>