--- a/src/HOL/Statespace/state_fun.ML Tue Apr 24 14:17:57 2018 +0000
+++ b/src/HOL/Statespace/state_fun.ML Tue Apr 24 14:17:58 2018 +0000
@@ -76,7 +76,7 @@
fun string_eq_simp_tac ctxt =
simp_tac (put_simpset HOL_basic_ss ctxt
- addsimps @{thms list.inject list.distinct Char_eq_Char_iff
+ addsimps @{thms list.inject list.distinct char.inject
cong_exp_iff_simps simp_thms}
addsimprocs [lazy_conj_simproc]
|> Simplifier.add_cong @{thm block_conj_cong});
@@ -85,7 +85,7 @@
val lookup_ss =
simpset_of (put_simpset HOL_basic_ss @{context}
- addsimps (@{thms list.inject} @ @{thms Char_eq_Char_iff}
+ addsimps (@{thms list.inject} @ @{thms char.inject}
@ @{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}])
@@ -161,7 +161,7 @@
val meta_ext = @{thm StateFun.meta_ext};
val ss' =
simpset_of (put_simpset HOL_ss @{context} addsimps
- (@{thm StateFun.update_apply} :: @{thm Fun.o_apply} :: @{thms list.inject} @ @{thms Char_eq_Char_iff}
+ (@{thm StateFun.update_apply} :: @{thm Fun.o_apply} :: @{thms list.inject} @ @{thms char.inject}
@ @{thms list.distinct})
addsimprocs [lazy_conj_simproc, StateSpace.distinct_simproc]
|> fold Simplifier.add_cong @{thms block_conj_cong});