# HG changeset patch
# User bulwahn
# Date 1328434977 -3600
# Node ID 51259911b9faf7c4985642372f766a7c66fc7577
# Parent  5ab496224729fe1d0278f959e18e22ea1b16737c
tuning to remove ML warnings

diff -r 5ab496224729 -r 51259911b9fa src/HOL/Tools/list_to_set_comprehension.ML
--- a/src/HOL/Tools/list_to_set_comprehension.ML	Sun Feb 05 08:57:03 2012 +0100
+++ b/src/HOL/Tools/list_to_set_comprehension.ML	Sun Feb 05 10:42:57 2012 +0100
@@ -82,7 +82,7 @@
         fun check (i, case_t) s =
           (case strip_abs_body case_t of
             (Const (@{const_name List.Nil}, _)) => s
-          | t => (case s of NONE => SOME i | SOME s => NONE))
+          | _ => (case s of NONE => SOME i | SOME _ => NONE))
       in
         fold_index check cases NONE
       end
@@ -132,7 +132,7 @@
           in
             (* do case distinction *)
             Splitter.split_tac [#split info] 1
-            THEN EVERY (map_index (fn (i', case_rewrite) =>
+            THEN EVERY (map_index (fn (i', _) =>
               (if i' < length (#case_rewrites info) - 1 then rtac @{thm conjI} 1 else all_tac)
               THEN REPEAT_DETERM (rtac @{thm allI} 1)
               THEN rtac @{thm impI} 1
@@ -207,7 +207,7 @@
                 val eqs' = map reverse_bounds eqs
                 val pat_eq' = reverse_bounds pat_eq
                 val inner_t =
-                  fold (fn (v, T) => fn t => HOLogic.exists_const T $ absdummy T t)
+                  fold (fn (_, T) => fn t => HOLogic.exists_const T $ absdummy T t)
                     (rev bound_vs) (fold (curry HOLogic.mk_conj) eqs' pat_eq')
                 val lhs = term_of redex
                 val rhs = HOLogic.mk_Collect ("x", rT, inner_t)