diff -r 0cd15d8c90a0 -r a2a1c8a658ef src/HOLCF/Fixrec.thy
--- a/src/HOLCF/Fixrec.thy	Sat May 22 10:02:07 2010 -0700
+++ b/src/HOLCF/Fixrec.thy	Sat May 22 12:36:50 2010 -0700
@@ -586,24 +586,4 @@
 
 hide_const (open) return fail run cases
 
-lemmas [fixrec_simp] =
-  beta_cfun cont2cont
-  run_strict run_fail run_return
-  mplus_strict mplus_fail mplus_return
-  spair_strict_iff
-  sinl_defined_iff
-  sinr_defined_iff
-  up_defined
-  ONE_defined
-  dist_eq_tr(1,2)
-  match_UU_simps
-  match_cpair_simps
-  match_spair_simps
-  match_sinl_simps
-  match_sinr_simps
-  match_up_simps
-  match_ONE_simps
-  match_TT_simps
-  match_FF_simps
-
 end