--- a/src/HOL/ex/Numeral.thy Mon Jan 10 08:18:49 2011 +0100
+++ b/src/HOL/ex/Numeral.thy Mon Jan 10 15:19:48 2011 +0100
@@ -588,7 +588,7 @@
simproc_setup numeral_minus ("of_num m - of_num n") = {*
let
(*TODO proper implicit use of morphism via pattern antiquotations*)
- fun cdest_of_num ct = (snd o split_last o snd o Drule.strip_comb) ct;
+ fun cdest_of_num ct = (List.last o snd o Drule.strip_comb) ct;
fun cdest_minus ct = case (rev o snd o Drule.strip_comb) ct of [n, m] => (m, n);
fun attach_num ct = (dest_num (Thm.term_of ct), ct);
fun cdifference t = (pairself (attach_num o cdest_of_num) o cdest_minus) t;