--- 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)