rename lambda translation schemes
authorblanchet
Mon Jan 30 17:15:59 2012 +0100 (2012-01-30)
changeset 46365547d1a1dcaf6
parent 46364 abab10d1f4a3
child 46366 2ded91a6cbd5
rename lambda translation schemes
src/HOL/IMP/Live_True.thy
src/HOL/Library/While_Combinator.thy
src/HOL/Mirabelle/Tools/mirabelle_metis.ML
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/TPTP/CASC_Setup.thy
src/HOL/TPTP/atp_theory_export.ML
src/HOL/Tools/ATP/atp_problem_generate.ML
src/HOL/Tools/ATP/atp_proof_reconstruct.ML
src/HOL/Tools/ATP/atp_systems.ML
src/HOL/Tools/Metis/metis_generate.ML
src/HOL/Tools/Metis/metis_tactic.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
src/HOL/ex/sledgehammer_tactics.ML
     1.1 --- a/src/HOL/IMP/Live_True.thy	Mon Jan 30 17:15:59 2012 +0100
     1.2 +++ b/src/HOL/IMP/Live_True.thy	Mon Jan 30 17:15:59 2012 +0100
     1.3 @@ -146,7 +146,7 @@
     1.4  lemma while_option_stop2:
     1.5   "while_option b c s = Some t \<Longrightarrow> EX k. t = (c^^k) s \<and> \<not> b t"
     1.6  apply(simp add: while_option_def split: if_splits)
     1.7 -by (metis (lam_lifting) LeastI_ex)
     1.8 +by (metis (lifting) LeastI_ex)
     1.9  (* move to While_Combinator *)
    1.10  lemma while_option_finite_subset_Some: fixes C :: "'a set"
    1.11    assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C"
     2.1 --- a/src/HOL/Library/While_Combinator.thy	Mon Jan 30 17:15:59 2012 +0100
     2.2 +++ b/src/HOL/Library/While_Combinator.thy	Mon Jan 30 17:15:59 2012 +0100
     2.3 @@ -55,7 +55,7 @@
     2.4  lemma while_option_stop2:
     2.5   "while_option b c s = Some t \<Longrightarrow> EX k. t = (c^^k) s \<and> \<not> b t"
     2.6  apply(simp add: while_option_def split: if_splits)
     2.7 -by (metis (lam_lifting) LeastI_ex)
     2.8 +by (metis (lifting) LeastI_ex)
     2.9  
    2.10  lemma while_option_stop: "while_option b c s = Some t \<Longrightarrow> ~ b t"
    2.11  by(metis while_option_stop2)
     3.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Mon Jan 30 17:15:59 2012 +0100
     3.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Mon Jan 30 17:15:59 2012 +0100
     3.3 @@ -19,7 +19,7 @@
     3.4      val facts = Facts.props (Proof_Context.facts_of (Proof.context_of pre))
     3.5  
     3.6      fun metis ctxt =
     3.7 -      Metis_Tactic.metis_tac [] ATP_Problem_Generate.lam_liftingN ctxt
     3.8 +      Metis_Tactic.metis_tac [] ATP_Problem_Generate.liftingN ctxt
     3.9                               (thms @ facts)
    3.10    in
    3.11      (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed")
     4.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Jan 30 17:15:59 2012 +0100
     4.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Jan 30 17:15:59 2012 +0100
     4.3 @@ -581,7 +581,7 @@
     4.4            ORELSE' sledge_tac 0.2 ATP_Systems.eN "mono_guards??"
     4.5            ORELSE' sledge_tac 0.2 ATP_Systems.vampireN "mono_guards??"
     4.6            ORELSE' sledge_tac 0.2 ATP_Systems.spassN "poly_tags"
     4.7 -          ORELSE' Metis_Tactic.metis_tac [] ATP_Problem_Generate.combinatorsN
     4.8 +          ORELSE' Metis_Tactic.metis_tac [] ATP_Problem_Generate.combsN
     4.9              ctxt thms
    4.10          else if !reconstructor = "smt" then
    4.11            SMT_Solver.smt_tac ctxt thms
     5.1 --- a/src/HOL/TPTP/CASC_Setup.thy	Mon Jan 30 17:15:59 2012 +0100
     5.2 +++ b/src/HOL/TPTP/CASC_Setup.thy	Mon Jan 30 17:15:59 2012 +0100
     5.3 @@ -129,7 +129,7 @@
     5.4                            Sledgehammer_Filter.no_relevance_override))
     5.5     ORELSE
     5.6     SOLVE_TIMEOUT (max_secs div 10) "metis"
     5.7 -       (ALLGOALS (Metis_Tactic.metis_tac [] ATP_Problem_Generate.lam_liftingN ctxt []))
     5.8 +       (ALLGOALS (Metis_Tactic.metis_tac [] ATP_Problem_Generate.liftingN ctxt []))
     5.9     ORELSE
    5.10     SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac ctxt))
    5.11     ORELSE
     6.1 --- a/src/HOL/TPTP/atp_theory_export.ML	Mon Jan 30 17:15:59 2012 +0100
     6.2 +++ b/src/HOL/TPTP/atp_theory_export.ML	Mon Jan 30 17:15:59 2012 +0100
     6.3 @@ -180,8 +180,8 @@
     6.4        |> map (fn ((_, loc), th) =>
     6.5                   ((Thm.get_name_hint th, loc),
     6.6                     th |> prop_of |> mono ? monomorphize_term ctxt))
     6.7 -      |> prepare_atp_problem ctxt format Axiom Axiom type_enc true combinatorsN
     6.8 -                             false true [] @{prop False}
     6.9 +      |> prepare_atp_problem ctxt format Axiom Axiom type_enc true combsN false
    6.10 +                             true [] @{prop False}
    6.11        |> #1
    6.12      val atp_problem =
    6.13        atp_problem
     7.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Jan 30 17:15:59 2012 +0100
     7.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Jan 30 17:15:59 2012 +0100
     7.3 @@ -34,9 +34,11 @@
     7.4    val type_tag_arguments : bool Config.T
     7.5    val no_lamsN : string
     7.6    val hide_lamsN : string
     7.7 +  val liftingN : string
     7.8 +  val combsN : string
     7.9 +  val combs_and_liftingN : string
    7.10 +  val combs_or_liftingN : string
    7.11    val lam_liftingN : string
    7.12 -  val combinatorsN : string
    7.13 -  val hybrid_lamsN : string
    7.14    val keep_lamsN : string
    7.15    val schematic_var_prefix : string
    7.16    val fixed_var_prefix : string
    7.17 @@ -123,10 +125,12 @@
    7.18  
    7.19  val no_lamsN = "no_lams" (* used internally; undocumented *)
    7.20  val hide_lamsN = "hide_lams"
    7.21 -val lam_liftingN = "lam_lifting"
    7.22 -val combinatorsN = "combinators"
    7.23 -val hybrid_lamsN = "hybrid_lams"
    7.24 +val liftingN = "lifting"
    7.25 +val combsN = "combs"
    7.26 +val combs_and_liftingN = "combs_and_lifting"
    7.27 +val combs_or_liftingN = "combs_or_lifting"
    7.28  val keep_lamsN = "keep_lams"
    7.29 +val lam_liftingN = "lam_lifting" (* legacy *)
    7.30  
    7.31  (* It's still unclear whether all TFF1 implementations will support type
    7.32     signatures such as "!>[A : $tType] : $o", with ghost type variables. *)
    7.33 @@ -1693,11 +1697,15 @@
    7.34      rpair []
    7.35    else if lam_trans = hide_lamsN then
    7.36      lift_lams ctxt type_enc ##> K []
    7.37 -  else if lam_trans = lam_liftingN then
    7.38 +  else if lam_trans = liftingN orelse lam_trans = lam_liftingN then
    7.39      lift_lams ctxt type_enc
    7.40 -  else if lam_trans = combinatorsN then
    7.41 +  else if lam_trans = combsN then
    7.42      map (introduce_combinators ctxt) #> rpair []
    7.43 -  else if lam_trans = hybrid_lamsN then
    7.44 +  else if lam_trans = combs_and_liftingN then
    7.45 +    lift_lams_part_1 ctxt type_enc
    7.46 +    ##> maps (fn t => [t, introduce_combinators ctxt (intentionalize_def t)])
    7.47 +    #> lift_lams_part_2
    7.48 +  else if lam_trans = combs_or_liftingN then (* ### FIXME: implement *)
    7.49      lift_lams_part_1 ctxt type_enc
    7.50      ##> maps (fn t => [t, introduce_combinators ctxt (intentionalize_def t)])
    7.51      #> lift_lams_part_2
     8.1 --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Jan 30 17:15:59 2012 +0100
     8.2 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Jan 30 17:15:59 2012 +0100
     8.3 @@ -121,7 +121,7 @@
     8.4  fun unalias_type_enc s =
     8.5    AList.lookup (op =) type_enc_aliases s |> the_default [s]
     8.6  
     8.7 -val metis_default_lam_trans = combinatorsN
     8.8 +val metis_default_lam_trans = combsN
     8.9  
    8.10  fun metis_call type_enc lam_trans =
    8.11    let
    8.12 @@ -175,9 +175,12 @@
    8.13    String.isSubstring ascii_of_lam_fact_prefix s
    8.14  
    8.15  fun lam_trans_from_atp_proof atp_proof default =
    8.16 -  if is_axiom_used_in_proof is_combinator_def atp_proof then combinatorsN
    8.17 -  else if is_axiom_used_in_proof is_lam_lifted atp_proof then lam_liftingN
    8.18 -  else default
    8.19 +  case (is_axiom_used_in_proof is_combinator_def atp_proof,
    8.20 +        is_axiom_used_in_proof is_lam_lifted atp_proof) of
    8.21 +    (false, false) => default
    8.22 +  | (false, true) => liftingN
    8.23 +  | (true, false) => combsN
    8.24 +  | (true, true) => combs_and_liftingN
    8.25  
    8.26  val is_typed_helper_name =
    8.27    String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix
     9.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Mon Jan 30 17:15:59 2012 +0100
     9.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon Jan 30 17:15:59 2012 +0100
     9.3 @@ -245,14 +245,14 @@
     9.4       let val method = effective_e_weight_method ctxt in
     9.5         (* FUDGE *)
     9.6         if method = e_smartN then
     9.7 -         [(0.333, (true, (500, FOF, "mono_tags??", combinatorsN,
     9.8 +         [(0.333, (true, (500, FOF, "mono_tags??", combsN,
     9.9                            e_fun_weightN))),
    9.10 -          (0.334, (true, (50, FOF, "mono_guards??", combinatorsN,
    9.11 +          (0.334, (true, (50, FOF, "mono_guards??", combsN,
    9.12                            e_fun_weightN))),
    9.13 -          (0.333, (true, (1000, FOF, "mono_tags??", combinatorsN,
    9.14 +          (0.333, (true, (1000, FOF, "mono_tags??", combsN,
    9.15                            e_sym_offset_weightN)))]
    9.16         else
    9.17 -         [(1.0, (true, (500, FOF, "mono_tags??", combinatorsN, method)))]
    9.18 +         [(1.0, (true, (500, FOF, "mono_tags??", combsN, method)))]
    9.19       end}
    9.20  
    9.21  val e = (eN, e_config)
    9.22 @@ -277,9 +277,9 @@
    9.23     prem_kind = Hypothesis,
    9.24     best_slices = fn ctxt =>
    9.25       (* FUDGE *)
    9.26 -     [(0.667, (false, (150, leo2_thf0, "mono_simple_higher", lam_liftingN,
    9.27 +     [(0.667, (false, (150, leo2_thf0, "mono_simple_higher", liftingN,
    9.28                         sosN))),
    9.29 -      (0.333, (true, (50, leo2_thf0, "mono_simple_higher", lam_liftingN,
    9.30 +      (0.333, (true, (50, leo2_thf0, "mono_simple_higher", liftingN,
    9.31                        no_sosN)))]
    9.32       |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
    9.33           else I)}
    9.34 @@ -335,11 +335,11 @@
    9.35     prem_kind = Conjecture,
    9.36     best_slices = fn ctxt =>
    9.37       (* FUDGE *)
    9.38 -     [(0.333, (false, (150, DFG DFG_Unsorted, "mono_tags??", lam_liftingN,
    9.39 +     [(0.333, (false, (150, DFG DFG_Unsorted, "mono_tags??", liftingN,
    9.40                         sosN))),
    9.41 -      (0.333, (false, (300, DFG DFG_Unsorted, "poly_tags??", lam_liftingN,
    9.42 +      (0.333, (false, (300, DFG DFG_Unsorted, "poly_tags??", liftingN,
    9.43                         sosN))),
    9.44 -      (0.334, (false, (50, DFG DFG_Unsorted, "mono_tags??", lam_liftingN,
    9.45 +      (0.334, (false, (50, DFG DFG_Unsorted, "mono_tags??", liftingN,
    9.46                         no_sosN)))]
    9.47       |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
    9.48           else I)}
    9.49 @@ -357,11 +357,11 @@
    9.50     prem_kind = #prem_kind spass_config,
    9.51     best_slices = fn ctxt =>
    9.52       (* FUDGE *)
    9.53 -     [(0.333, (false, (150, DFG DFG_Sorted, "mono_simple", lam_liftingN,
    9.54 +     [(0.333, (false, (150, DFG DFG_Sorted, "mono_simple", liftingN,
    9.55                         sosN))) (*,
    9.56 -      (0.333, (false, (300, DFG DFG_Sorted, "poly_tags??", lam_liftingN,
    9.57 +      (0.333, (false, (300, DFG DFG_Sorted, "poly_tags??", liftingN,
    9.58                         sosN))),
    9.59 -      (0.334, (true, (50, DFG DFG_Sorted, "mono_simple", lam_liftingN,
    9.60 +      (0.334, (true, (50, DFG DFG_Sorted, "mono_simple", liftingN,
    9.61                        no_sosN)))*)]
    9.62       |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
    9.63           else I)}
    9.64 @@ -404,15 +404,15 @@
    9.65     best_slices = fn ctxt =>
    9.66       (* FUDGE *)
    9.67       (if is_old_vampire_version () then
    9.68 -        [(0.333, (false, (150, FOF, "poly_guards??", hybrid_lamsN, sosN))),
    9.69 -         (0.333, (false, (500, FOF, "mono_tags??", hybrid_lamsN, sosN))),
    9.70 -         (0.334, (true, (50, FOF, "mono_guards??", hybrid_lamsN, no_sosN)))]
    9.71 +        [(0.333, (false, (150, FOF, "poly_guards??", combs_or_liftingN, sosN))),
    9.72 +         (0.333, (false, (500, FOF, "mono_tags??", combs_or_liftingN, sosN))),
    9.73 +         (0.334, (true, (50, FOF, "mono_guards??", combs_or_liftingN, no_sosN)))]
    9.74        else
    9.75 -        [(0.333, (false, (150, vampire_tff0, "poly_guards??", hybrid_lamsN,
    9.76 +        [(0.333, (false, (150, vampire_tff0, "poly_guards??", combs_or_liftingN,
    9.77                            sosN))),
    9.78 -         (0.333, (false, (500, vampire_tff0, "mono_simple", hybrid_lamsN,
    9.79 +         (0.333, (false, (500, vampire_tff0, "mono_simple", combs_or_liftingN,
    9.80                            sosN))),
    9.81 -         (0.334, (true, (50, vampire_tff0, "mono_simple", hybrid_lamsN,
    9.82 +         (0.334, (true, (50, vampire_tff0, "mono_simple", combs_or_liftingN,
    9.83                           no_sosN)))])
    9.84       |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
    9.85           else I)}
    9.86 @@ -435,10 +435,10 @@
    9.87     prem_kind = Hypothesis,
    9.88     best_slices =
    9.89       (* FUDGE *)
    9.90 -     K [(0.5, (false, (250, z3_tff0, "mono_simple", combinatorsN, ""))),
    9.91 -        (0.25, (false, (125, z3_tff0, "mono_simple", combinatorsN, ""))),
    9.92 -        (0.125, (false, (62, z3_tff0, "mono_simple", combinatorsN, ""))),
    9.93 -        (0.125, (false, (31, z3_tff0, "mono_simple", combinatorsN, "")))]}
    9.94 +     K [(0.5, (false, (250, z3_tff0, "mono_simple", combsN, ""))),
    9.95 +        (0.25, (false, (125, z3_tff0, "mono_simple", combsN, ""))),
    9.96 +        (0.125, (false, (62, z3_tff0, "mono_simple", combsN, ""))),
    9.97 +        (0.125, (false, (31, z3_tff0, "mono_simple", combsN, "")))]}
    9.98  
    9.99  val z3_tptp = (z3_tptpN, z3_tptp_config)
   9.100  
   9.101 @@ -456,7 +456,7 @@
   9.102     best_slices =
   9.103       K [(1.0, (false, (200, format, type_enc,
   9.104                         if is_format_higher_order format then keep_lamsN
   9.105 -                       else combinatorsN, "")))]}
   9.106 +                       else combsN, "")))]}
   9.107  
   9.108  val dummy_tff1_format = TFF (TPTP_Polymorphic, TPTP_Explicit)
   9.109  val dummy_tff1_config = dummy_config dummy_tff1_format "poly_simple"
   9.110 @@ -537,43 +537,43 @@
   9.111  
   9.112  val remote_e =
   9.113    remotify_atp e "EP" ["1.0", "1.1", "1.2"]
   9.114 -      (K (750, FOF, "mono_tags??", combinatorsN) (* FUDGE *))
   9.115 +      (K (750, FOF, "mono_tags??", combsN) (* FUDGE *))
   9.116  val remote_leo2 =
   9.117    remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
   9.118 -      (K (100, leo2_thf0, "mono_simple_higher", lam_liftingN) (* FUDGE *))
   9.119 +      (K (100, leo2_thf0, "mono_simple_higher", liftingN) (* FUDGE *))
   9.120  val remote_satallax =
   9.121    remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
   9.122        (K (100, satallax_thf0, "mono_simple_higher", keep_lamsN) (* FUDGE *))
   9.123  val remote_vampire =
   9.124    remotify_atp vampire "Vampire" ["1.8"]
   9.125 -      (K (250, FOF, "mono_guards??", hybrid_lamsN) (* FUDGE *))
   9.126 +      (K (250, FOF, "mono_guards??", combs_or_liftingN) (* FUDGE *))
   9.127  val remote_z3_tptp =
   9.128    remotify_atp z3_tptp "Z3" ["3.0"]
   9.129 -      (K (250, z3_tff0, "mono_simple", combinatorsN) (* FUDGE *))
   9.130 +      (K (250, z3_tff0, "mono_simple", combsN) (* FUDGE *))
   9.131  val remote_e_sine =
   9.132    remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
   9.133 -      Conjecture (K (500, FOF, "mono_guards??", combinatorsN) (* FUDGE *))
   9.134 +      Conjecture (K (500, FOF, "mono_guards??", combsN) (* FUDGE *))
   9.135  val remote_iprover =
   9.136    remote_atp iproverN "iProver" [] [] [] Axiom Conjecture
   9.137 -      (K (150, FOF, "mono_guards??", lam_liftingN) (* FUDGE *))
   9.138 +      (K (150, FOF, "mono_guards??", liftingN) (* FUDGE *))
   9.139  val remote_iprover_eq =
   9.140    remote_atp iprover_eqN "iProver-Eq" [] [] [] Axiom Conjecture
   9.141 -      (K (150, FOF, "mono_guards??", lam_liftingN) (* FUDGE *))
   9.142 +      (K (150, FOF, "mono_guards??", liftingN) (* FUDGE *))
   9.143  val remote_snark =
   9.144    remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
   9.145        [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
   9.146 -      (K (100, explicit_tff0, "mono_simple", lam_liftingN) (* FUDGE *))
   9.147 +      (K (100, explicit_tff0, "mono_simple", liftingN) (* FUDGE *))
   9.148  val remote_e_tofof =
   9.149    remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Axiom
   9.150        Hypothesis
   9.151 -      (K (150, explicit_tff0, "mono_simple", lam_liftingN) (* FUDGE *))
   9.152 +      (K (150, explicit_tff0, "mono_simple", liftingN) (* FUDGE *))
   9.153  val remote_waldmeister =
   9.154    remote_atp waldmeisterN "Waldmeister" ["710"]
   9.155        [("#START OF PROOF", "Proved Goals:")]
   9.156        [(OutOfResources, "Too many function symbols"),
   9.157         (Crashed, "Unrecoverable Segmentation Fault")]
   9.158        Hypothesis Hypothesis
   9.159 -      (K (50, CNF_UEQ, "mono_tags??", combinatorsN) (* FUDGE *))
   9.160 +      (K (50, CNF_UEQ, "mono_tags??", combsN) (* FUDGE *))
   9.161  
   9.162  (* Setup *)
   9.163  
    10.1 --- a/src/HOL/Tools/Metis/metis_generate.ML	Mon Jan 30 17:15:59 2012 +0100
    10.2 +++ b/src/HOL/Tools/Metis/metis_generate.ML	Mon Jan 30 17:15:59 2012 +0100
    10.3 @@ -230,7 +230,8 @@
    10.4        fold_rev (fn (name, th) => fn (old_skolems, props) =>
    10.5                     th |> prop_of |> Logic.strip_imp_concl
    10.6                        |> conceal_old_skolem_terms (length clauses) old_skolems
    10.7 -                      ||> lam_trans = lam_liftingN ? eliminate_lam_wrappers
    10.8 +                      ||> (lam_trans = liftingN orelse lam_trans = lam_liftingN)
    10.9 +                          ? eliminate_lam_wrappers
   10.10                        ||> (fn prop => (name, prop) :: props))
   10.11                 clauses ([], [])
   10.12      (*
   10.13 @@ -238,7 +239,7 @@
   10.14        tracing ("PROPS:\n" ^
   10.15                 cat_lines (map (Syntax.string_of_term ctxt o snd) props))
   10.16      *)
   10.17 -    val lam_trans = if lam_trans = combinatorsN then no_lamsN else lam_trans
   10.18 +    val lam_trans = if lam_trans = combsN then no_lamsN else lam_trans
   10.19      val (atp_problem, _, _, lifted, sym_tab) =
   10.20        prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc false lam_trans
   10.21                            false false [] @{prop False} props
    11.1 --- a/src/HOL/Tools/Metis/metis_tactic.ML	Mon Jan 30 17:15:59 2012 +0100
    11.2 +++ b/src/HOL/Tools/Metis/metis_tactic.ML	Mon Jan 30 17:15:59 2012 +0100
    11.3 @@ -125,13 +125,15 @@
    11.4    let val thy = Proof_Context.theory_of ctxt
    11.5        val new_skolemizer =
    11.6          Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy)
    11.7 -      val do_lams = lam_trans = lam_liftingN ? introduce_lam_wrappers ctxt
    11.8 +      val do_lams =
    11.9 +        (lam_trans = liftingN orelse lam_trans = lam_liftingN)
   11.10 +        ? introduce_lam_wrappers ctxt
   11.11        val th_cls_pairs =
   11.12          map2 (fn j => fn th =>
   11.13                  (Thm.get_name_hint th,
   11.14                   th |> Drule.eta_contraction_rule
   11.15                      |> Meson_Clausify.cnf_axiom ctxt new_skolemizer
   11.16 -                                                (lam_trans = combinatorsN) j
   11.17 +                                                (lam_trans = combsN) j
   11.18                      ||> map do_lams))
   11.19               (0 upto length ths0 - 1) ths0
   11.20        val ths = maps (snd o snd) th_cls_pairs
   11.21 @@ -247,7 +249,7 @@
   11.22      else
   11.23        ();
   11.24      Meson.MESON (preskolem_tac ctxt)
   11.25 -        (maps (neg_clausify ctxt (lam_trans = combinatorsN))) tac ctxt i st0
   11.26 +        (maps (neg_clausify ctxt (lam_trans = combsN))) tac ctxt i st0
   11.27    end
   11.28  
   11.29  fun metis_tac [] = generic_metis_tac partial_type_encs
   11.30 @@ -277,7 +279,7 @@
   11.31                                                 (schem_facts @ ths))
   11.32    end
   11.33  
   11.34 -val metis_lam_transs = [hide_lamsN, lam_liftingN, combinatorsN]
   11.35 +val metis_lam_transs = [hide_lamsN, liftingN, combsN]
   11.36  
   11.37  fun set_opt _ x NONE = SOME x
   11.38    | set_opt get x (SOME x0) =
    12.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Jan 30 17:15:59 2012 +0100
    12.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Jan 30 17:15:59 2012 +0100
    12.3 @@ -134,7 +134,7 @@
    12.4  val das_tool = "Sledgehammer"
    12.5  
    12.6  val reconstructor_names = [metisN, smtN]
    12.7 -val plain_metis = Metis (hd partial_type_encs, combinatorsN)
    12.8 +val plain_metis = Metis (hd partial_type_encs, combsN)
    12.9  val is_reconstructor = member (op =) reconstructor_names
   12.10  
   12.11  val is_atp = member (op =) o supported_atps
   12.12 @@ -991,8 +991,7 @@
   12.13                  state subgoal SMT
   12.14                  (bunch_of_reconstructors false
   12.15                       (fn plain =>
   12.16 -                         if plain then metis_default_lam_trans
   12.17 -                         else lam_liftingN)),
   12.18 +                         if plain then metis_default_lam_trans else liftingN)),
   12.19           fn preplay =>
   12.20              let
   12.21                val one_line_params =
    13.1 --- a/src/HOL/ex/sledgehammer_tactics.ML	Mon Jan 30 17:15:59 2012 +0100
    13.2 +++ b/src/HOL/ex/sledgehammer_tactics.ML	Mon Jan 30 17:15:59 2012 +0100
    13.3 @@ -71,7 +71,7 @@
    13.4  fun sledgehammer_with_metis_tac ctxt override_params relevance_override i th =
    13.5    case run_atp override_params relevance_override i i ctxt th of
    13.6      SOME facts =>
    13.7 -    Metis_Tactic.metis_tac [] ATP_Problem_Generate.combinatorsN ctxt
    13.8 +    Metis_Tactic.metis_tac [] ATP_Problem_Generate.combsN ctxt
    13.9          (maps (thms_of_name ctxt) facts) i th
   13.10    | NONE => Seq.empty
   13.11