# HG changeset patch
# User blanchet
# Date 1327996367 -3600
# Node ID d724066ff3d01a64fd9f3b0aba678d141d06cd20
# Parent  10c5f39ec7764b78e1c7466c745383f20ee1785e
reverted e2b1a86d59fc -- broke Metis's lambda-lifting

diff -r 10c5f39ec776 -r d724066ff3d0 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jan 31 07:11:20 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jan 31 08:52:47 2012 +0100
@@ -690,6 +690,15 @@
     (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
@@ -699,7 +708,7 @@
                     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)) =
@@ -1674,15 +1683,6 @@
 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,
@@ -1749,7 +1749,7 @@
                         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