--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Sun Mar 28 16:13:29 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Sun Mar 28 16:59:06 2010 +0200
@@ -27,7 +27,7 @@
val trace = Unsynchronized.ref false;
fun trace_msg msg = if !trace then tracing (msg ()) else ();
-val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" true;
+val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true);
datatype mode = FO | HO | FT (* first-order, higher-order, fully-typed *)