diff -r cd9df61fee34 -r 93b32361d398 src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML	Sat Jan 18 12:43:24 2025 +0100
+++ b/src/HOL/Import/import_rule.ML	Sat Jan 18 12:45:33 2025 +0100
@@ -367,10 +367,6 @@
     val thy' = #2 (Global_Theory.add_thm ((binding, th'), []) thy)
   in State (thy', a, b, c) end
 
-fun list_last (x :: y :: zs) = apfst (fn t => x :: y :: t) (list_last zs)
-  | list_last [x] = ([], x)
-  | list_last [] = raise Fail "list_last: empty"
-
 fun pair_list (x :: y :: zs) = ((x, y) :: pair_list zs)
   | pair_list [] = []
   | pair_list _ = raise Fail "pair_list: odd list length"
@@ -396,10 +392,10 @@
   | command (#"L", [t, th]) = term t ##>> thm th #>> uncurry abs #-> set_thm
   | command (#"M", [s]) = get_thm s #-> set_thm
   | command (#"Q", args) =
-      list_last args |> (fn (tys, th) => thm th #-> (fn th => typs tys #-> (fn tys =>
+      split_last args |> (fn (tys, th) => thm th #-> (fn th => typs tys #-> (fn tys =>
         set_thm (inst_type (pair_list tys) th))))
   | command (#"S", args) =
-      list_last args |> (fn (ts, th) => thm th #-> (fn th => terms ts #-> (fn ts =>
+      split_last args |> (fn (ts, th) => thm th #-> (fn th => terms ts #-> (fn ts =>
         set_thm (inst (pair_list ts) th))))
   | command (#"F", [name, t]) =
       term t #-> (fn t => theory_op (def (make_name name) t) #-> set_thm)