1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Nov 15 22:20:58 2011 +0100
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Nov 16 09:42:27 2011 +0100
     1.3 @@ -11,7 +11,7 @@
     1.4  val type_encK = "type_enc"
     1.5  val soundK = "sound"
     1.6  val slicingK = "slicing"
     1.7 -val lambda_transK = "lambda_trans"
     1.8 +val lam_transK = "lam_trans"
     1.9  val e_weight_methodK = "e_weight_method"
    1.10  val force_sosK = "force_sos"
    1.11  val max_relevantK = "max_relevant"
    1.12 @@ -355,7 +355,7 @@
    1.13    SH_FAIL of int * int |
    1.14    SH_ERROR
    1.15  
    1.16 -fun run_sh prover_name prover type_enc sound max_relevant slicing lambda_trans
    1.17 +fun run_sh prover_name prover type_enc sound max_relevant slicing lam_trans
    1.18          e_weight_method force_sos hard_timeout timeout dir pos st =
    1.19    let
    1.20      val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
    1.21 @@ -371,9 +371,6 @@
    1.22      val st' =
    1.23        st |> Proof.map_context
    1.24                  (set_file_name dir
    1.25 -                 #> (Option.map (Config.put
    1.26 -                       Sledgehammer_Provers.atp_lambda_trans)
    1.27 -                       lambda_trans |> the_default I)
    1.28                   #> (Option.map (Config.put ATP_Systems.e_weight_method)
    1.29                         e_weight_method |> the_default I)
    1.30                   #> (Option.map (Config.put ATP_Systems.force_sos)
    1.31 @@ -383,6 +380,7 @@
    1.32            [("verbose", "true"),
    1.33             ("type_enc", type_enc),
    1.34             ("sound", sound),
    1.35 +           ("lam_trans", lam_trans |> the_default "smart"),
    1.36             ("preplay_timeout", preplay_timeout),
    1.37             ("max_relevant", max_relevant),
    1.38             ("slicing", slicing),
    1.39 @@ -465,7 +463,7 @@
    1.40      val sound = AList.lookup (op =) args soundK |> the_default "false"
    1.41      val max_relevant = AList.lookup (op =) args max_relevantK |> the_default "smart"
    1.42      val slicing = AList.lookup (op =) args slicingK |> the_default "true"
    1.43 -    val lambda_trans = AList.lookup (op =) args lambda_transK
    1.44 +    val lam_trans = AList.lookup (op =) args lam_transK
    1.45      val e_weight_method = AList.lookup (op =) args e_weight_methodK
    1.46      val force_sos = AList.lookup (op =) args force_sosK
    1.47        |> Option.map (curry (op <>) "false")
    1.48 @@ -475,7 +473,7 @@
    1.49         minimizer has a chance to do its magic *)
    1.50      val hard_timeout = SOME (2 * timeout)
    1.51      val (msg, result) =
    1.52 -      run_sh prover_name prover type_enc sound max_relevant slicing lambda_trans
    1.53 +      run_sh prover_name prover type_enc sound max_relevant slicing lam_trans
    1.54          e_weight_method force_sos hard_timeout timeout dir pos st
    1.55    in
    1.56      case result of
    1.57 @@ -576,15 +574,17 @@
    1.58            ORELSE' sledge_tac 0.2 ATP_Systems.eN "mono_guards??"
    1.59            ORELSE' sledge_tac 0.2 ATP_Systems.vampireN "mono_guards??"
    1.60            ORELSE' sledge_tac 0.2 ATP_Systems.spassN "poly_tags"
    1.61 -          ORELSE' Metis_Tactic.metis_tac [] ctxt thms
    1.62 +          ORELSE' Metis_Tactic.metis_tac [] ATP_Translate.combinatorsN ctxt thms
    1.63          else if !reconstructor = "smt" then
    1.64            SMT_Solver.smt_tac ctxt thms
    1.65          else if full orelse !reconstructor = "metis (full_types)" then
    1.66 -          Metis_Tactic.metis_tac [Metis_Tactic.full_type_enc] ctxt thms
    1.67 +          Metis_Tactic.metis_tac [Metis_Tactic.full_type_enc]
    1.68 +                                 ATP_Translate.combinatorsN ctxt thms
    1.69          else if !reconstructor = "metis (no_types)" then
    1.70 -          Metis_Tactic.metis_tac [Metis_Tactic.no_type_enc] ctxt thms
    1.71 +          Metis_Tactic.metis_tac [Metis_Tactic.no_type_enc]
    1.72 +                                 ATP_Translate.combinatorsN ctxt thms
    1.73          else if !reconstructor = "metis" then
    1.74 -          Metis_Tactic.metis_tac [] ctxt thms
    1.75 +          Metis_Tactic.metis_tac [] ATP_Translate.combinatorsN ctxt thms
    1.76          else
    1.77            K all_tac
    1.78        end

     2.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Nov 15 22:20:58 2011 +0100
     2.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Nov 16 09:42:27 2011 +0100
     2.3 @@ -90,13 +90,13 @@
     2.4    val is_type_enc_fairly_sound : type_enc -> bool
     2.5    val type_enc_from_string : soundness -> string -> type_enc
     2.6    val adjust_type_enc : atp_format -> type_enc -> type_enc
     2.7 -  val lift_lambdas :
     2.8 -    Proof.context -> type_enc -> term list -> term list * term list
     2.9    val mk_aconns :
    2.10      connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
    2.11    val unmangled_const : string -> string * (string, 'b) ho_term list
    2.12    val unmangled_const_name : string -> string
    2.13    val helper_table : ((string * bool) * thm list) list
    2.14 +  val trans_lams_from_string :
    2.15 +    Proof.context -> type_enc -> string -> term list -> term list * term list
    2.16    val factsN : string
    2.17    val prepare_atp_problem :
    2.18      Proof.context -> atp_format -> formula_kind -> formula_kind -> type_enc
    2.19 @@ -690,7 +690,7 @@
    2.20      open_form (subst_bound (Var ((s, 0), T), t))
    2.21    | open_form t = t
    2.22  
    2.23 -fun lift_lambdas ctxt type_enc =
    2.24 +fun lift_lams ctxt type_enc =
    2.25    map (Envir.eta_contract #> close_form) #> rpair ctxt
    2.26    #-> Lambda_Lifting.lift_lambdas
    2.27            (SOME (if polymorphism_of_type_enc type_enc = Polymorphic then
    2.28 @@ -1165,10 +1165,10 @@
    2.29    handle THM _ => t |> do_cheaply_conceal_lambdas Ts
    2.30  val introduce_combinators = simple_translate_lambdas do_introduce_combinators
    2.31  
    2.32 -fun preprocess_abstractions_in_terms trans_lambdas facts =
    2.33 +fun preprocess_abstractions_in_terms trans_lams facts =
    2.34    let
    2.35      val (facts, lambda_ts) =
    2.36 -      facts |> map (snd o snd) |> trans_lambdas
    2.37 +      facts |> map (snd o snd) |> trans_lams
    2.38              |>> map2 (fn (name, (kind, _)) => fn t => (name, (kind, t))) facts
    2.39      val lambda_facts =
    2.40        map2 (fn t => fn j =>
    2.41 @@ -1677,28 +1677,28 @@
    2.42      end
    2.43    | extract_lambda_def _ = raise Fail "malformed lifted lambda"
    2.44  
    2.45 -fun translate_formulas ctxt format prem_kind type_enc lambda_trans presimp
    2.46 -                       hyp_ts concl_t facts =
    2.47 +fun trans_lams_from_string ctxt type_enc lam_trans =
    2.48 +  if lam_trans = no_lamsN then
    2.49 +    rpair []
    2.50 +  else if lam_trans = hide_lamsN then
    2.51 +    lift_lams ctxt type_enc ##> K []
    2.52 +  else if lam_trans = lam_liftingN then
    2.53 +    lift_lams ctxt type_enc
    2.54 +  else if lam_trans = combinatorsN then
    2.55 +    map (introduce_combinators ctxt) #> rpair []
    2.56 +  else if lam_trans = hybrid_lamsN then
    2.57 +    lift_lams ctxt type_enc
    2.58 +    ##> maps (fn t => [t, introduce_combinators ctxt (intentionalize_def t)])
    2.59 +  else if lam_trans = keep_lamsN then
    2.60 +    map (Envir.eta_contract) #> rpair []
    2.61 +  else
    2.62 +    error ("Unknown lambda translation method: " ^ quote lam_trans ^ ".")
    2.63 +
    2.64 +fun translate_formulas ctxt format prem_kind type_enc lam_trans presimp hyp_ts
    2.65 +                       concl_t facts =
    2.66    let
    2.67      val thy = Proof_Context.theory_of ctxt
    2.68 -    val trans_lambdas =
    2.69 -      if lambda_trans = no_lamsN then
    2.70 -        rpair []
    2.71 -      else if lambda_trans = hide_lamsN then
    2.72 -        lift_lambdas ctxt type_enc ##> K []
    2.73 -      else if lambda_trans = lam_liftingN then
    2.74 -        lift_lambdas ctxt type_enc
    2.75 -      else if lambda_trans = combinatorsN then
    2.76 -        map (introduce_combinators ctxt) #> rpair []
    2.77 -      else if lambda_trans = hybrid_lamsN then
    2.78 -        lift_lambdas ctxt type_enc
    2.79 -        ##> maps (fn t => [t, introduce_combinators ctxt
    2.80 -                                  (intentionalize_def t)])
    2.81 -      else if lambda_trans = keep_lamsN then
    2.82 -        map (Envir.eta_contract) #> rpair []
    2.83 -      else
    2.84 -        error ("Unknown lambda translation method: " ^
    2.85 -               quote lambda_trans ^ ".")
    2.86 +    val trans_lams = trans_lams_from_string ctxt type_enc lam_trans
    2.87      val presimp_consts = Meson.presimplified_consts ctxt
    2.88      val fact_ts = facts |> map snd
    2.89      (* Remove existing facts from the conjecture, as this can dramatically
    2.90 @@ -1715,11 +1715,11 @@
    2.91        (conjs, facts)
    2.92        |> presimp
    2.93           ? pairself (map (apsnd (uncurry (presimp_prop ctxt presimp_consts))))
    2.94 -      |> (if lambda_trans = no_lamsN then
    2.95 +      |> (if lam_trans = no_lamsN then
    2.96              rpair []
    2.97            else
    2.98              op @
    2.99 -            #> preprocess_abstractions_in_terms trans_lambdas
   2.100 +            #> preprocess_abstractions_in_terms trans_lams
   2.101              #>> chop (length conjs))
   2.102      val conjs = conjs |> make_conjecture ctxt format type_enc
   2.103      val (fact_names, facts) =
   2.104 @@ -2330,7 +2330,7 @@
   2.105  val explicit_apply_threshold = 50
   2.106  
   2.107  fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc exporter
   2.108 -        lambda_trans readable_names preproc hyp_ts concl_t facts =
   2.109 +                        lam_trans readable_names preproc hyp_ts concl_t facts =
   2.110    let
   2.111      val thy = Proof_Context.theory_of ctxt
   2.112      val type_enc = type_enc |> adjust_type_enc format
   2.113 @@ -2343,19 +2343,19 @@
   2.114          NONE
   2.115        else
   2.116          SOME false
   2.117 -    val lambda_trans =
   2.118 -      if lambda_trans = smartN then
   2.119 +    val lam_trans =
   2.120 +      if lam_trans = smartN then
   2.121          if is_type_enc_higher_order type_enc then keep_lamsN else combinatorsN
   2.122 -      else if lambda_trans = keep_lamsN andalso
   2.123 +      else if lam_trans = keep_lamsN andalso
   2.124                not (is_type_enc_higher_order type_enc) then
   2.125          error ("Lambda translation method incompatible with first-order \
   2.126                 \encoding.")
   2.127        else
   2.128 -        lambda_trans
   2.129 +        lam_trans
   2.130      val (fact_names, classes, conjs, facts, class_rel_clauses, arity_clauses,
   2.131           lifted) =
   2.132 -      translate_formulas ctxt format prem_kind type_enc lambda_trans preproc
   2.133 -                         hyp_ts concl_t facts
   2.134 +      translate_formulas ctxt format prem_kind type_enc lam_trans preproc hyp_ts
   2.135 +                         concl_t facts
   2.136      val sym_tab =
   2.137        sym_table_for_facts ctxt type_enc explicit_apply conjs facts
   2.138      val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc

     3.1 --- a/src/HOL/Tools/Metis/metis_tactic.ML	Tue Nov 15 22:20:58 2011 +0100
     3.2 +++ b/src/HOL/Tools/Metis/metis_tactic.ML	Wed Nov 16 09:42:27 2011 +0100
     3.3 @@ -23,7 +23,8 @@
     3.4    val verbose : bool Config.T
     3.5    val new_skolemizer : bool Config.T
     3.6    val type_has_top_sort : typ -> bool
     3.7 -  val metis_tac : string list -> Proof.context -> thm list -> int -> tactic
     3.8 +  val metis_tac :
     3.9 +    string list -> string -> Proof.context -> thm list -> int -> tactic
    3.10    val setup : theory -> theory
    3.11  end
    3.12  
    3.13 @@ -53,11 +54,15 @@
    3.14     (partial_typesN, partial_type_syss),
    3.15     (no_typesN, [no_type_enc])]
    3.16  
    3.17 -fun method_call_for_type_enc type_syss =
    3.18 +val lam_transs = [hide_lamsN, lam_liftingN, combinatorsN]
    3.19 +val default_lam_trans = combinatorsN
    3.20 +
    3.21 +fun method_call_for type_syss lam_trans =
    3.22    metisN ^ " (" ^
    3.23    (case AList.find (op =) type_enc_aliases type_syss of
    3.24       [alias] => alias
    3.25 -   | _ => hd type_syss) ^ ")"
    3.26 +   | _ => hd type_syss) ^
    3.27 +  (if lam_trans = default_lam_trans then "" else ", " ^ lam_trans) ^ ")"
    3.28  
    3.29  val new_skolemizer =
    3.30    Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
    3.31 @@ -130,7 +135,7 @@
    3.32  val resolution_params = {active = active_params, waiting = waiting_params}
    3.33  
    3.34  (* Main function to start Metis proof and reconstruction *)
    3.35 -fun FOL_SOLVE (type_enc :: fallback_type_syss) lambda_trans ctxt cls ths0 =
    3.36 +fun FOL_SOLVE (type_enc :: fallback_type_syss) lam_trans ctxt cls ths0 =
    3.37    let val thy = Proof_Context.theory_of ctxt
    3.38        val new_skolemizer =
    3.39          Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy)
    3.40 @@ -138,7 +143,7 @@
    3.41          map2 (fn j => fn th =>
    3.42                  (Thm.get_name_hint th,
    3.43                   Meson_Clausify.cnf_axiom ctxt new_skolemizer
    3.44 -                                          (lambda_trans = combinatorsN) j th))
    3.45 +                                          (lam_trans = combinatorsN) j th))
    3.46               (0 upto length ths0 - 1) ths0
    3.47        val ths = maps (snd o snd) th_cls_pairs
    3.48        val dischargers = map (fst o snd) th_cls_pairs
    3.49 @@ -147,13 +152,13 @@
    3.50        val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
    3.51        val type_enc = type_enc_from_string Sound type_enc
    3.52        val (sym_tab, axioms, concealed) =
    3.53 -        prepare_metis_problem ctxt type_enc lambda_trans cls ths
    3.54 +        prepare_metis_problem ctxt type_enc lam_trans cls ths
    3.55        fun get_isa_thm mth Isa_Reflexive_or_Trivial =
    3.56            reflexive_or_trivial_from_metis ctxt type_enc sym_tab concealed mth
    3.57          | get_isa_thm mth Isa_Lambda_Lifted =
    3.58            lambda_lifted_from_metis ctxt type_enc sym_tab concealed mth
    3.59          | get_isa_thm _ (Isa_Raw ith) =
    3.60 -          ith |> lambda_trans = lam_liftingN
    3.61 +          ith |> lam_trans = lam_liftingN
    3.62                   ? introduce_lambda_wrappers_in_theorem ctxt
    3.63        val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith))
    3.64        val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES")
    3.65 @@ -221,8 +226,8 @@
    3.66           | _ =>
    3.67             (verbose_warning ctxt
    3.68                  ("Falling back on " ^
    3.69 -                 quote (method_call_for_type_enc fallback_type_syss) ^ "...");
    3.70 -            FOL_SOLVE fallback_type_syss lambda_trans ctxt cls ths0)
    3.71 +                 quote (method_call_for fallback_type_syss lam_trans) ^ "...");
    3.72 +            FOL_SOLVE fallback_type_syss lam_trans ctxt cls ths0)
    3.73  
    3.74  fun neg_clausify ctxt combinators =
    3.75    single
    3.76 @@ -241,21 +246,20 @@
    3.77  val type_has_top_sort =
    3.78    exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
    3.79  
    3.80 -fun generic_metis_tac type_syss ctxt ths i st0 =
    3.81 +fun generic_metis_tac type_syss lam_trans ctxt ths i st0 =
    3.82    let
    3.83 -    val lambda_trans = Config.get ctxt lambda_trans
    3.84      val _ = trace_msg ctxt (fn () =>
    3.85          "Metis called with theorems\n" ^
    3.86          cat_lines (map (Display.string_of_thm ctxt) ths))
    3.87      fun tac clause =
    3.88 -      resolve_tac (FOL_SOLVE type_syss lambda_trans ctxt clause ths) 1
    3.89 +      resolve_tac (FOL_SOLVE type_syss lam_trans ctxt clause ths) 1
    3.90    in
    3.91      if exists_type type_has_top_sort (prop_of st0) then
    3.92        verbose_warning ctxt "Proof state contains the universal sort {}"
    3.93      else
    3.94        ();
    3.95      Meson.MESON (preskolem_tac ctxt)
    3.96 -        (maps (neg_clausify ctxt (lambda_trans = combinatorsN))) tac ctxt i st0
    3.97 +        (maps (neg_clausify ctxt (lam_trans = combinatorsN))) tac ctxt i st0
    3.98    end
    3.99  
   3.100  fun metis_tac [] = generic_metis_tac partial_type_syss
   3.101 @@ -269,7 +273,7 @@
   3.102  val has_tvar =
   3.103    exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of
   3.104  
   3.105 -fun method default_type_syss (override_type_syss, ths) ctxt facts =
   3.106 +fun method default_type_syss ((override_type_syss, lam_trans), ths) ctxt facts =
   3.107    let
   3.108      val _ =
   3.109        if default_type_syss = full_type_syss then
   3.110 @@ -278,16 +282,28 @@
   3.111          ()
   3.112      val (schem_facts, nonschem_facts) = List.partition has_tvar facts
   3.113      val type_syss = override_type_syss |> the_default default_type_syss
   3.114 +    val lam_trans = lam_trans |> the_default default_lam_trans
   3.115    in
   3.116      HEADGOAL (Method.insert_tac nonschem_facts THEN'
   3.117 -              CHANGED_PROP
   3.118 -              o generic_metis_tac type_syss ctxt (schem_facts @ ths))
   3.119 +              CHANGED_PROP o generic_metis_tac type_syss lam_trans ctxt
   3.120 +                                               (schem_facts @ ths))
   3.121    end
   3.122  
   3.123 +fun consider_arg s =
   3.124 +  if member (op =) lam_transs s then
   3.125 +    apsnd (K (SOME s))
   3.126 +  else
   3.127 +    apfst (K (SOME (AList.lookup (op =) type_enc_aliases s |> the_default [s])))
   3.128 +
   3.129  fun setup_method (binding, type_syss) =
   3.130 -  ((Args.parens (Scan.repeat Parse.short_ident)
   3.131 -    >> maps (fn s => AList.lookup (op =) type_enc_aliases s |> the_default [s]))
   3.132 -    |> Scan.option |> Scan.lift)
   3.133 +  (Scan.lift (Scan.optional
   3.134 +       (Args.parens (Parse.short_ident
   3.135 +                     -- Scan.option (Parse.$$$ "," |-- Parse.short_ident))
   3.136 +        >> (fn (s, s') =>
   3.137 +               (NONE, NONE)
   3.138 +               |> consider_arg s
   3.139 +               |> (case s' of SOME s' => consider_arg s' | _ => I)))
   3.140 +       (NONE, NONE)))
   3.141    -- Attrib.thms >> (METHOD oo method type_syss)
   3.142    |> Method.setup binding
   3.143  

     4.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Tue Nov 15 22:20:58 2011 +0100
     4.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Wed Nov 16 09:42:27 2011 +0100
     4.3 @@ -24,7 +24,6 @@
     4.4    val metis_generated_var_prefix : string
     4.5    val trace : bool Config.T
     4.6    val verbose : bool Config.T
     4.7 -  val lambda_trans : string Config.T
     4.8    val trace_msg : Proof.context -> (unit -> string) -> unit
     4.9    val verbose_warning : Proof.context -> string -> unit
    4.10    val metis_name_table : ((string * int) * ((type_enc -> string) * bool)) list
    4.11 @@ -52,8 +51,6 @@
    4.12  
    4.13  val trace = Attrib.setup_config_bool @{binding metis_trace} (K false)
    4.14  val verbose = Attrib.setup_config_bool @{binding metis_verbose} (K true)
    4.15 -val lambda_trans =
    4.16 -  Attrib.setup_config_string @{binding metis_lambda_trans} (K combinatorsN)
    4.17  
    4.18  fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
    4.19  fun verbose_warning ctxt msg =
    4.20 @@ -202,7 +199,7 @@
    4.21    | metis_axiom_from_atp _ _ _ = raise Fail "not CNF -- expected formula"
    4.22  
    4.23  (* Function to generate metis clauses, including comb and type clauses *)
    4.24 -fun prepare_metis_problem ctxt type_enc lambda_trans conj_clauses fact_clauses =
    4.25 +fun prepare_metis_problem ctxt type_enc lam_trans conj_clauses fact_clauses =
    4.26    let
    4.27      val (conj_clauses, fact_clauses) =
    4.28        if polymorphism_of_type_enc type_enc = Polymorphic then
    4.29 @@ -232,10 +229,9 @@
    4.30        tracing ("PROPS:\n" ^
    4.31                 cat_lines (map (Syntax.string_of_term ctxt o snd) props))
    4.32      *)
    4.33 -    val lambda_trans =
    4.34 -      if lambda_trans = combinatorsN then no_lamsN else lambda_trans
    4.35 +    val lam_trans = if lam_trans = combinatorsN then no_lamsN else lam_trans
    4.36      val (atp_problem, _, _, _, _, _, lifted, sym_tab) =
    4.37 -      prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc false lambda_trans
    4.38 +      prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc false lam_trans
    4.39                            false false [] @{prop False} props
    4.40      (*
    4.41      val _ = tracing ("ATP PROBLEM: " ^

     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Nov 15 22:20:58 2011 +0100
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Nov 16 09:42:27 2011 +0100
     5.3 @@ -87,6 +87,7 @@
     5.4     ("blocking", "false"),
     5.5     ("type_enc", "smart"),
     5.6     ("sound", "false"),
     5.7 +   ("lam_trans", "smart"),
     5.8     ("relevance_thresholds", "0.45 0.85"),
     5.9     ("max_relevant", "smart"),
    5.10     ("max_mono_iters", "3"),
    5.11 @@ -108,9 +109,9 @@
    5.12     ("no_slicing", "slicing")]
    5.13  
    5.14  val params_for_minimize =
    5.15 -  ["debug", "verbose", "overlord", "type_enc", "sound", "max_mono_iters",
    5.16 -   "max_new_mono_instances", "isar_proof", "isar_shrink_factor", "timeout",
    5.17 -   "preplay_timeout"]
    5.18 +  ["debug", "verbose", "overlord", "type_enc", "sound", "lam_trans",
    5.19 +   "max_mono_iters", "max_new_mono_instances", "isar_proof",
    5.20 +   "isar_shrink_factor", "timeout", "preplay_timeout"]
    5.21  
    5.22  val property_dependent_params = ["provers", "timeout"]
    5.23  
    5.24 @@ -137,8 +138,10 @@
    5.25                              | _ => value)
    5.26      | NONE => (name, value)
    5.27  
    5.28 -(* "provers =" and "type_enc =" can be left out. The latter is a secret
    5.29 -   feature. *)
    5.30 +val any_type_enc = type_enc_from_string Sound "erased"
    5.31 +
    5.32 +(* "provers =", "type_enc =", and "lam_trans" can be omitted. For the last two,
    5.33 +   this is a secret feature. *)
    5.34  fun normalize_raw_param ctxt =
    5.35    unalias_raw_param
    5.36    #> (fn (name, value) =>
    5.37 @@ -148,6 +151,9 @@
    5.38             ("provers", [name])
    5.39           else if can (type_enc_from_string Sound) name andalso null value then
    5.40             ("type_enc", [name])
    5.41 +         else if can (trans_lams_from_string ctxt any_type_enc) name andalso
    5.42 +                 null value then
    5.43 +           ("lam_trans", [name])
    5.44           else
    5.45             error ("Unknown parameter: " ^ quote name ^ "."))
    5.46  
    5.47 @@ -275,6 +281,7 @@
    5.48          "smart" => NONE
    5.49        | s => (type_enc_from_string Sound s; SOME s)
    5.50      val sound = mode = Auto_Try orelse lookup_bool "sound"
    5.51 +    val lam_trans = lookup_string "lam_trans"
    5.52      val relevance_thresholds = lookup_real_pair "relevance_thresholds"
    5.53      val max_relevant = lookup_option lookup_int "max_relevant"
    5.54      val max_mono_iters = lookup_int "max_mono_iters"
    5.55 @@ -290,10 +297,10 @@
    5.56      val expect = lookup_string "expect"
    5.57    in
    5.58      {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
    5.59 -     provers = provers, relevance_thresholds = relevance_thresholds,
    5.60 +     provers = provers, type_enc = type_enc, sound = sound,
    5.61 +     lam_trans = lam_trans, relevance_thresholds = relevance_thresholds,
    5.62       max_relevant = max_relevant, max_mono_iters = max_mono_iters,
    5.63 -     max_new_mono_instances = max_new_mono_instances, type_enc = type_enc,
    5.64 -     sound = sound, isar_proof = isar_proof,
    5.65 +     max_new_mono_instances = max_new_mono_instances,  isar_proof = isar_proof,
    5.66       isar_shrink_factor = isar_shrink_factor, slicing = slicing,
    5.67       timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
    5.68    end

     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Tue Nov 15 22:20:58 2011 +0100
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Nov 16 09:42:27 2011 +0100
     6.3 @@ -47,7 +47,7 @@
     6.4  fun print silent f = if silent then () else Output.urgent_message (f ())
     6.5  
     6.6  fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
     6.7 -                 max_new_mono_instances, type_enc, isar_proof,
     6.8 +                 max_new_mono_instances, type_enc, lam_trans, isar_proof,
     6.9                   isar_shrink_factor, preplay_timeout, ...} : params)
    6.10                 silent (prover : prover) timeout i n state facts =
    6.11    let
    6.12 @@ -62,8 +62,8 @@
    6.13      val params =
    6.14        {debug = debug, verbose = verbose, overlord = overlord, blocking = true,
    6.15         provers = provers, type_enc = type_enc, sound = true,
    6.16 -       relevance_thresholds = (1.01, 1.01), max_relevant = SOME (length facts),
    6.17 -       max_mono_iters = max_mono_iters,
    6.18 +       lam_trans = lam_trans, relevance_thresholds = (1.01, 1.01),
    6.19 +       max_relevant = SOME (length facts), max_mono_iters = max_mono_iters,
    6.20         max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
    6.21         isar_shrink_factor = isar_shrink_factor, slicing = false,
    6.22         timeout = timeout, preplay_timeout = preplay_timeout, expect = ""}

     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Nov 15 22:20:58 2011 +0100
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Nov 16 09:42:27 2011 +0100
     7.3 @@ -26,6 +26,7 @@
     7.4       provers: string list,
     7.5       type_enc: string option,
     7.6       sound: bool,
     7.7 +     lam_trans: string,
     7.8       relevance_thresholds: real * real,
     7.9       max_relevant: int option,
    7.10       max_mono_iters: int,
    7.11 @@ -62,7 +63,6 @@
    7.12  
    7.13    val dest_dir : string Config.T
    7.14    val problem_prefix : string Config.T
    7.15 -  val atp_lambda_trans : string Config.T
    7.16    val atp_full_names : bool Config.T
    7.17    val smt_triggers : bool Config.T
    7.18    val smt_weights : bool Config.T
    7.19 @@ -297,6 +297,7 @@
    7.20     provers: string list,
    7.21     type_enc: string option,
    7.22     sound: bool,
    7.23 +   lam_trans: string,
    7.24     relevance_thresholds: real * real,
    7.25     max_relevant: int option,
    7.26     max_mono_iters: int,
    7.27 @@ -339,8 +340,6 @@
    7.28  val problem_prefix =
    7.29    Attrib.setup_config_string @{binding sledgehammer_problem_prefix} (K "prob")
    7.30  
    7.31 -val atp_lambda_trans =
    7.32 -  Attrib.setup_config_string @{binding sledgehammer_atp_lambda_trans} (K smartN)
    7.33  (* In addition to being easier to read, readable names are often much shorter,
    7.34     especially if types are mangled in names. This makes a difference for some
    7.35     provers (e.g., E). For these reason, short names are enabled by default. *)
    7.36 @@ -412,11 +411,11 @@
    7.37    in TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end
    7.38  
    7.39  fun tac_for_reconstructor Metis =
    7.40 -    Metis_Tactic.metis_tac [Metis_Tactic.partial_type_enc]
    7.41 +    Metis_Tactic.metis_tac [Metis_Tactic.partial_type_enc] combinatorsN
    7.42    | tac_for_reconstructor Metis_Full_Types =
    7.43 -    Metis_Tactic.metis_tac Metis_Tactic.full_type_syss
    7.44 +    Metis_Tactic.metis_tac Metis_Tactic.full_type_syss combinatorsN
    7.45    | tac_for_reconstructor Metis_No_Types =
    7.46 -    Metis_Tactic.metis_tac [Metis_Tactic.no_type_enc]
    7.47 +    Metis_Tactic.metis_tac [Metis_Tactic.no_type_enc] combinatorsN
    7.48    | tac_for_reconstructor SMT = SMT_Solver.smt_tac
    7.49  
    7.50  fun timed_reconstructor reconstructor debug timeout ths =
    7.51 @@ -561,7 +560,7 @@
    7.52  fun run_atp mode name
    7.53          ({exec, required_execs, arguments, proof_delims, known_failures,
    7.54            conj_sym_kind, prem_kind, best_slices, ...} : atp_config)
    7.55 -        ({debug, verbose, overlord, type_enc, sound, max_relevant,
    7.56 +        ({debug, verbose, overlord, type_enc, sound, lam_trans, max_relevant,
    7.57            max_mono_iters, max_new_mono_instances, isar_proof,
    7.58            isar_shrink_factor, slicing, timeout, preplay_timeout, ...} : params)
    7.59          minimize_command
    7.60 @@ -670,12 +669,12 @@
    7.61                      |> Output.urgent_message
    7.62                    else
    7.63                      ()
    7.64 +                val readable_names = not (Config.get ctxt atp_full_names)
    7.65                  val (atp_problem, pool, conjecture_offset, facts_offset,
    7.66                       fact_names, typed_helpers, _, sym_tab) =
    7.67                    prepare_atp_problem ctxt format conj_sym_kind prem_kind
    7.68 -                      type_enc false (Config.get ctxt atp_lambda_trans)
    7.69 -                      (not (Config.get ctxt atp_full_names)) true hyp_ts concl_t
    7.70 -                      facts
    7.71 +                      type_enc false lam_trans readable_names true hyp_ts
    7.72 +                      concl_t facts
    7.73                  fun weights () = atp_problem_weights atp_problem
    7.74                  val full_proof = debug orelse isar_proof
    7.75                  val core =

     8.1 --- a/src/HOL/ex/sledgehammer_tactics.ML	Tue Nov 15 22:20:58 2011 +0100
     8.2 +++ b/src/HOL/ex/sledgehammer_tactics.ML	Wed Nov 16 09:42:27 2011 +0100
     8.3 @@ -71,7 +71,8 @@
     8.4  fun sledgehammer_with_metis_tac ctxt override_params relevance_override i th =
     8.5    case run_atp override_params relevance_override i i ctxt th of
     8.6      SOME facts =>
     8.7 -    Metis_Tactic.metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th
     8.8 +    Metis_Tactic.metis_tac [] ATP_Translate.combinatorsN ctxt
     8.9 +        (maps (thms_of_name ctxt) facts) i th
    8.10    | NONE => Seq.empty
    8.11  
    8.12  fun sledgehammer_as_oracle_tac ctxt override_params relevance_override i th =