--- 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});