# HG changeset patch # User wenzelm # Date 1213025485 -7200 # Node ID 2a91d9575935e721cbd2968d752ea962aa0cc313 # Parent d89fb4ee72802d528f51594070a9f7f476e75f42 DatatypePackage.distinct_simproc; diff -r d89fb4ee7280 -r 2a91d9575935 src/HOL/Statespace/state_fun.ML --- a/src/HOL/Statespace/state_fun.ML Mon Jun 09 17:24:48 2008 +0200 +++ b/src/HOL/Statespace/state_fun.ML Mon Jun 09 17:31:25 2008 +0200 @@ -75,7 +75,7 @@ val string_eq_simp_tac = simp_tac (HOL_basic_ss addsimps (thms "list.inject"@thms "char.inject"@simp_thms) - addsimprocs [distinct_simproc,lazy_conj_simproc] + addsimprocs [DatatypePackage.distinct_simproc,lazy_conj_simproc] addcongs [thm "block_conj_cong"]) end; @@ -90,7 +90,7 @@ in val lookup_ss = (HOL_basic_ss addsimps (thms "list.inject"@thms "char.inject"@simp_thms@rules) - addsimprocs [distinct_simproc,lazy_conj_simproc] + addsimprocs [DatatypePackage.distinct_simproc,lazy_conj_simproc] addcongs [thm "block_conj_cong"] addSolver StateSpace.distinctNameSolver) end; @@ -168,7 +168,7 @@ val meta_ext = thm "StateFun.meta_ext"; val o_apply = thm "Fun.o_apply"; val ss' = (HOL_ss addsimps (update_apply::o_apply::thms "list.inject"@thms "char.inject") - addsimprocs [distinct_simproc,lazy_conj_simproc,StateSpace.distinct_simproc] + addsimprocs [DatatypePackage.distinct_simproc,lazy_conj_simproc,StateSpace.distinct_simproc] addcongs [thm "block_conj_cong"]); in val update_simproc =