--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Fri May 21 17:16:16 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Sat May 22 08:30:40 2010 -0700
@@ -34,11 +34,11 @@
structure Domain_Isomorphism : DOMAIN_ISOMORPHISM =
struct
-val beta_ss =
- HOL_basic_ss
- addsimps simp_thms
- addsimps [@{thm beta_cfun}]
- addsimprocs [@{simproc cont_proc}];
+val beta_rules =
+ @{thms beta_cfun cont_id cont_const cont2cont_Rep_CFun cont2cont_LAM'} @
+ @{thms cont2cont_fst cont2cont_snd cont2cont_Pair cont2cont_split'};
+
+val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules);
val beta_tac = simp_tac beta_ss;