# HG changeset patch
# User wenzelm
# Date 1737027948 -3600
# Node ID 6c60f773033f5f5b82f31a017c01dcc204fb34aa
# Parent  ca1ad6660b4a82290b7caeadf07ec90b2dffcfa7
tuned;

diff -r ca1ad6660b4a -r 6c60f773033f src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML	Thu Jan 16 12:41:55 2025 +0100
+++ b/src/HOL/Import/import_rule.ML	Thu Jan 16 12:45:48 2025 +0100
@@ -289,13 +289,9 @@
        |> forall_elim_list rng
   end
 
-fun transl_dotc #"." = "dot"
-  | transl_dotc c = Char.toString c
-val transl_dot = String.translate transl_dotc
+val transl_dot = String.translate (fn #"." => "dot" | c => Char.toString c)
 
-fun transl_qmc #"?" = "t"
-  | transl_qmc c = Char.toString c
-val transl_qm = String.translate transl_qmc
+val transl_qm = String.translate (fn #"?" => "t" | c => Char.toString c)
 
 fun getconstname s thy =
   case Import_Data.get_const_map s thy of
@@ -418,7 +414,7 @@
           end
       | process (thy, state) (#"Y", [name, _, _]) = setth (mtydef name thy) (thy, state)
       | process (thy, state) (#"t", [n]) =
-          setty (Thm.global_ctyp_of thy (TFree ("'" ^ (transl_qm n), \<^sort>\<open>type\<close>))) (thy, state)
+          setty (Thm.global_ctyp_of thy (TFree ("'" ^ transl_qm n, \<^sort>\<open>type\<close>))) (thy, state)
       | process (thy, state) (#"a", n :: l) =
           fold_map getty l (thy, state) |>>
             (fn tys => Thm.global_ctyp_of thy (Type (gettyname n thy, map Thm.typ_of tys))) |-> setty