# HG changeset patch
# User wenzelm
# Date 1737410031 -3600
# Node ID 0a1ed07a458a39220dd2fa69f1cf8b30848242c6
# Parent  3c888cd24351d812ab9c8cc1afec9a0a09ecddac
cleanup generated bounds;

diff -r 3c888cd24351 -r 0a1ed07a458a src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML	Mon Jan 20 12:11:36 2025 +0100
+++ b/src/HOL/Import/import_rule.ML	Mon Jan 20 22:53:51 2025 +0100
@@ -310,6 +310,11 @@
 fun make_name hol =
   {hol = hol, isabelle = String.translate (fn #"." => "dot" | c => Char.toString c) hol}
 
+fun make_bound a =
+  (case try (unprefix "_") a of
+    SOME b => if forall_string Symbol.is_ascii_digit b then "u" else b
+  | NONE => a);
+
 fun make_free x ty = Thm.free (#isabelle (make_name x), ty);
 
 fun make_tfree thy a =
@@ -436,7 +441,9 @@
   | command (#"v", [x, ty]) = typ ty #>> make_free x #-> set_term
   | command (#"c", [c, ty]) = theory #-> (fn thy => typ ty #>> make_const thy c #-> set_term)
   | command (#"f", [t, u]) = term t #-> (fn t => term u #-> (fn u => set_term (Thm.apply t u)))
-  | command (#"l", [x, t]) = term x #-> (fn x => term t #-> (fn t => set_term (Thm.lambda x t)))
+  | command (#"l", [x, t]) =
+      term x #-> (fn x => term t #-> (fn t =>
+        set_term (Thm.lambda_name (make_bound (#1 (dest_Free (Thm.term_of x))), x) t)))
   | command (#"+", [name]) = store_thm (make_name name)
   | command (c, _) = raise Fail ("process: unknown command: " ^ String.str c)