# HG changeset patch
# User bulwahn
# Date 1285836489 -7200
# Node ID 371e9b5b23c260258aa856efb806c564e135febf
# Parent  9e59b4c11039d9dd38c8e0e256065eb3969f5ada
removing dead code

diff -r 9e59b4c11039 -r 371e9b5b23c2 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Thu Sep 30 09:31:07 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Thu Sep 30 10:48:09 2010 +0200
@@ -187,8 +187,6 @@
             val (assms, concl) = Logic.strip_horn (prop_of split_thm)
             val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl) 
             val subst = Pattern.match thy (split_t, t) (Vartab.empty, Vartab.empty)
-            val (_, split_args) = strip_comb split_t
-            val match = split_args ~~ args
             fun flatten_of_assm assm =
               let
                 val (vTs, assm') = strip_all (Envir.beta_norm (Envir.subst_term subst assm))