--- a/src/HOL/Tools/Metis/metis_translate.ML Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Mon Jun 06 20:36:35 2011 +0200
@@ -346,7 +346,8 @@
end
| metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula"
-val default_type_sys = Preds (Polymorphic, Nonmonotonic_Types, Lightweight)
+(* FIXME: put in "Metis_Tactics" as string *)
+val default_type_sys = Preds (Polymorphic, Const_Arg_Types, Lightweight)
(* Function to generate metis clauses, including comb and type clauses *)
fun prepare_metis_problem ctxt MX type_sys conj_clauses fact_clauses =