Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
removing dead code
authorbulwahn
Thu, 30 Sep 2010 10:48:09 +0200
changeset 39797 371e9b5b23c2
parent 39795 9e59b4c11039
child 39798 9e7a0a9d194e
removing dead code
src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML file | annotate | diff | comparison | revisions 
--- 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))
isabelle