# HG changeset patch
# User blanchet
# Date 1321613232 -3600
# Node ID 9c335d69a36249d0f93812195c93b71609c00d66
# Parent  2231a151db59f456d5a2a156c79545c8b89a5459
fixed bugs in lambda-lifting code -- ensure distinct names for variables

diff -r 2231a151db59 -r 9c335d69a362 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Fri Nov 18 11:47:12 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Fri Nov 18 11:47:12 2011 +0100
@@ -684,10 +684,11 @@
     (if String.isPrefix lam_lifted_prefix s then Const else Free) x
   | constify_lifted t = t
 
-(* Requires bound variables to have distinct names and 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)) =
-    open_form (subst_bound (Var ((s, 0), 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 (_, T, t)) =
+    subst_bound (Var ((Name.uu ^ Int.toString (size_of_term t), 0), T), t)
+    |> open_form
   | open_form t = t
 
 fun lift_lams_part_1 ctxt type_enc =
diff -r 2231a151db59 -r 9c335d69a362 src/HOL/Tools/Metis/metis_translate.ML
--- a/src/HOL/Tools/Metis/metis_translate.ML	Fri Nov 18 11:47:12 2011 +0100
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Fri Nov 18 11:47:12 2011 +0100
@@ -116,7 +116,8 @@
                    case AList.lookup (op =) lambdas s of
                      SOME t =>
                      Const (@{const_name Metis.lambda}, dummyT)
-                     $ map_types (map_type_tvar (K dummyT)) t
+                     $ map_types (map_type_tvar (K dummyT))
+                                 (reveal_lambda_lifted lambdas t)
                    | NONE => t
                  else
                    t