--- a/src/HOL/Tools/list_to_set_comprehension.ML Sun Jan 09 21:33:41 2011 +0100
+++ b/src/HOL/Tools/list_to_set_comprehension.ML Mon Jan 10 08:18:48 2011 +0100
@@ -59,8 +59,6 @@
datatype termlets = If | Case of (typ * int)
-val last = snd o split_last
-
fun meta_eq th = th RS @{thm eq_reflection}
fun rewr_conv' th = Conv.rewr_conv (meta_eq th)
@@ -100,7 +98,7 @@
SOME i =>
let
val (Ts, _) = strip_type T
- val T' = last Ts
+ val T' = snd (split_last Ts)
in SOME (snd (split_last args), T', i, nth args i) end
| NONE => NONE)
| NONE => NONE)