src/HOL/Statespace/state_fun.ML
changeset 27099 2a91d9575935
parent 26496 49ae9456eba9
child 27330 1af2598b5f7d
--- 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 =