# HG changeset patch
# User blanchet
# Date 1409695588 -7200
# Node ID e333bd3b4d3d34c18f54b54c99b28f6f3deff711
# Parent  14dda84afbb30615fff33fc88b98039fe23d613a
removed vacuous theorem references

diff -r 14dda84afbb3 -r e333bd3b4d3d src/HOL/Statespace/state_fun.ML
--- a/src/HOL/Statespace/state_fun.ML	Wed Sep 03 00:06:27 2014 +0200
+++ b/src/HOL/Statespace/state_fun.ML	Wed Sep 03 00:06:28 2014 +0200
@@ -78,8 +78,7 @@
 
 fun string_eq_simp_tac ctxt =
   simp_tac (put_simpset HOL_basic_ss ctxt
-    addsimps (@{thms list.inject} @ @{thms char.inject}
-      @ @{thms list.distinct} @ @{thms char.distinct} @ @{thms simp_thms})
+    addsimps (@{thms list.inject} @ @{thms char.inject} @ @{thms list.distinct} @ @{thms simp_thms})
     addsimprocs [lazy_conj_simproc]
     |> Simplifier.add_cong @{thm block_conj_cong});
 
@@ -88,7 +87,7 @@
 val lookup_ss =
   simpset_of (put_simpset HOL_basic_ss @{context}
     addsimps (@{thms list.inject} @ @{thms char.inject}
-      @ @{thms list.distinct} @ @{thms char.distinct} @ @{thms simp_thms}
+      @ @{thms list.distinct} @ @{thms simp_thms}
       @ [@{thm StateFun.lookup_update_id_same}, @{thm StateFun.id_id_cancel},
         @{thm StateFun.lookup_update_same}, @{thm StateFun.lookup_update_other}])
     addsimprocs [lazy_conj_simproc]
@@ -164,7 +163,7 @@
 val ss' =
   simpset_of (put_simpset HOL_ss @{context} addsimps
     (@{thm StateFun.update_apply} :: @{thm Fun.o_apply} :: @{thms list.inject} @ @{thms char.inject}
-      @ @{thms list.distinct} @ @{thms char.distinct})
+      @ @{thms list.distinct})
     addsimprocs [lazy_conj_simproc, StateSpace.distinct_simproc]
     |> fold Simplifier.add_cong @{thms block_conj_cong});