dropped unused binding
authorhaftmann
Thu Jan 14 17:54:55 2010 +0100 (2010-01-14)
changeset 34903d75704c60768
parent 34902 780172c006e1
child 34904 9c4d5db7c7ad
dropped unused binding
src/HOL/Tools/inductive_set.ML
     1.1 --- a/src/HOL/Tools/inductive_set.ML	Thu Jan 14 17:54:54 2010 +0100
     1.2 +++ b/src/HOL/Tools/inductive_set.ML	Thu Jan 14 17:54:55 2010 +0100
     1.3 @@ -34,7 +34,7 @@
     1.4  val collect_mem_simproc =
     1.5    Simplifier.simproc (theory "Set") "Collect_mem" ["Collect t"] (fn thy => fn ss =>
     1.6      fn S as Const ("Collect", Type ("fun", [_, T])) $ t =>
     1.7 -         let val (u, Ts, ps) = HOLogic.strip_psplits t
     1.8 +         let val (u, _, ps) = HOLogic.strip_psplits t
     1.9           in case u of
    1.10             (c as Const ("op :", _)) $ q $ S' =>
    1.11               (case try (HOLogic.strip_ptuple ps) q of