diff -r 25388cf06437 -r 973bb7846505 src/HOL/Tools/Metis/metis_translate.ML
--- a/src/HOL/Tools/Metis/metis_translate.ML	Tue Nov 15 22:20:58 2011 +0100
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Wed Nov 16 09:42:27 2011 +0100
@@ -24,7 +24,6 @@
   val metis_generated_var_prefix : string
   val trace : bool Config.T
   val verbose : bool Config.T
-  val lambda_trans : string Config.T
   val trace_msg : Proof.context -> (unit -> string) -> unit
   val verbose_warning : Proof.context -> string -> unit
   val metis_name_table : ((string * int) * ((type_enc -> string) * bool)) list
@@ -52,8 +51,6 @@
 
 val trace = Attrib.setup_config_bool @{binding metis_trace} (K false)
 val verbose = Attrib.setup_config_bool @{binding metis_verbose} (K true)
-val lambda_trans =
-  Attrib.setup_config_string @{binding metis_lambda_trans} (K combinatorsN)
 
 fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
 fun verbose_warning ctxt msg =
@@ -202,7 +199,7 @@
   | metis_axiom_from_atp _ _ _ = raise Fail "not CNF -- expected formula"
 
 (* Function to generate metis clauses, including comb and type clauses *)
-fun prepare_metis_problem ctxt type_enc lambda_trans conj_clauses fact_clauses =
+fun prepare_metis_problem ctxt type_enc lam_trans conj_clauses fact_clauses =
   let
     val (conj_clauses, fact_clauses) =
       if polymorphism_of_type_enc type_enc = Polymorphic then
@@ -232,10 +229,9 @@
       tracing ("PROPS:\n" ^
                cat_lines (map (Syntax.string_of_term ctxt o snd) props))
     *)
-    val lambda_trans =
-      if lambda_trans = combinatorsN then no_lamsN else lambda_trans
+    val lam_trans = if lam_trans = combinatorsN then no_lamsN else lam_trans
     val (atp_problem, _, _, _, _, _, lifted, sym_tab) =
-      prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc false lambda_trans
+      prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc false lam_trans
                           false false [] @{prop False} props
     (*
     val _ = tracing ("ATP PROBLEM: " ^