src/HOL/Tools/Metis/metis_generate.ML

       else if String.isPrefix conjecture_prefix ident then
         NONE
       else if String.isPrefix helper_prefix ident then
         (case (String.isSuffix typed_helper_suffix ident, space_explode "_" ident) of
           (needs_fairly_sound, _ :: const :: j :: _) =>
-          nth (AList.lookup (op =) helper_table (const, needs_fairly_sound) |> the)
+          nth (AList.lookup (op =) (helper_table true) (const, needs_fairly_sound) |> the)
             (the (Int.fromString j) - 1)
           |> snd |> prepare_helper ctxt
           |> Isa_Raw |> some
         | _ => raise Fail ("malformed helper identifier " ^ quote ident))
       else

         (0 upto length fact_clauses - 1) fact_clauses
     val (old_skolems, props) =
       fold_rev (fn (name, th) => fn (old_skolems, props) =>
            th |> Thm.prop_of |> Logic.strip_imp_concl
               |> conceal_old_skolem_terms (length clauses) old_skolems
-              ||> (lam_trans = liftingN orelse lam_trans = lam_liftingN) ? eliminate_lam_wrappers
+              ||> lam_trans = liftingN ? eliminate_lam_wrappers
               ||> (fn prop => (name, prop) :: props))
          clauses ([], [])
     (*
     val _ =
       tracing ("PROPS:\n" ^