# HG changeset patch
# User haftmann
# Date 1263488095 -3600
# Node ID d75704c60768fdc4b0785ca4076c80348e9a3be6
# Parent  780172c006e15b53ca95b383284af052692f58ce
dropped unused binding

diff -r 780172c006e1 -r d75704c60768 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Thu Jan 14 17:54:54 2010 +0100
+++ b/src/HOL/Tools/inductive_set.ML	Thu Jan 14 17:54:55 2010 +0100
@@ -34,7 +34,7 @@
 val collect_mem_simproc =
   Simplifier.simproc (theory "Set") "Collect_mem" ["Collect t"] (fn thy => fn ss =>
     fn S as Const ("Collect", Type ("fun", [_, T])) $ t =>
-         let val (u, Ts, ps) = HOLogic.strip_psplits t
+         let val (u, _, ps) = HOLogic.strip_psplits t
          in case u of
            (c as Const ("op :", _)) $ q $ S' =>
              (case try (HOLogic.strip_ptuple ps) q of