# HG changeset patch
# User bulwahn
# Date 1294643928 -3600
# Node ID e7c1248e39d08cfef8b0ed90d6d1355db6794d63
# Parent  82c1e348bc18ee92ef5be2936c33e981904bd284
made SML/NJ happy

diff -r 82c1e348bc18 -r e7c1248e39d0 src/HOL/Tools/list_to_set_comprehension.ML
--- 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)