# 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 =