src/HOL/Tools/ATP/atp_problem_generate.ML

   | constify_lifted (Abs (s, T, t)) = Abs (s, T, constify_lifted t)
   | constify_lifted (Free (x as (s, _))) =
     (if String.isPrefix lam_lifted_prefix s then Const else Free) x
   | constify_lifted t = t
 
+(* Requires bound variables not to clash with any schematic variables (as should
+   be the case right after lambda-lifting). *)
+fun open_form (Const (@{const_name All}, _) $ Abs (s, T, t)) =
+    let
+      val names = Name.make_context (map fst (Term.add_var_names t []))
+      val (s, _) = Name.variant s names
+    in open_form (subst_bound (Var ((s, 0), T), t)) end
+  | open_form t = t
+
 fun lift_lams_part_1 ctxt type_enc =
   map close_form #> rpair ctxt
   #-> Lambda_Lifting.lift_lambdas
           (SOME ((if polymorphism_of_type_enc type_enc = Polymorphic then
                     lam_lifted_poly_prefix
                   else
                     lam_lifted_mono_prefix) ^ "_a"))
           Lambda_Lifting.is_quantifier
   #> fst
-val lift_lams_part_2 = pairself (map constify_lifted)
+val lift_lams_part_2 = pairself (map (open_form o constify_lifted))
 val lift_lams = lift_lams_part_2 ooo lift_lams_part_1
 
 fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) =
     intentionalize_def t
   | intentionalize_def (Const (@{const_name HOL.eq}, _) $ t $ u) =

   in add end
 
 fun type_constrs_of_terms thy ts =
   Symtab.keys (fold (add_type_constrs_in_term thy) ts Symtab.empty)
 
-(* Requires bound variables not to clash with any schematic variables (as should
-   be the case right after lambda-lifting). *)
-fun open_form (Const (@{const_name All}, _) $ Abs (s, T, t)) =
-    let
-      val names = Name.make_context (map fst (Term.add_var_names t []))
-      val (s, _) = Name.variant s names
-    in open_form (subst_bound (Var ((s, 0), T), t)) end
-  | open_form t = t
-
 fun extract_lambda_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
     let val (head, args) = strip_comb t in
       (head |> dest_Const |> fst,
        fold_rev (fn t as Var ((s, _), T) =>
                     (fn u => Abs (s, T, abstract_over (t, u)))

       facts
       |> map_filter (fn (name, (_, t)) =>
                         make_fact ctxt format type_enc true (name, t)
                         |> Option.map (pair name))
       |> ListPair.unzip
-    val lifted = lam_facts |> map (extract_lambda_def o open_form o snd o snd)
+    val lifted = lam_facts |> map (extract_lambda_def o snd o snd)
     val lam_facts =
       lam_facts |> map_filter (make_fact ctxt format type_enc true o apsnd snd)
     val all_ts = concl_t :: hyp_ts @ fact_ts
     val subs = tfree_classes_of_terms all_ts
     val supers = tvar_classes_of_terms all_ts