src/HOL/HOLCF/ex/Pattern_Match.thy
changeset 40834 a1249aeff5b6
parent 40774 0437dbc127b3
child 41229 d797baa3d57c
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Tue Nov 30 15:34:51 2010 -0800
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Tue Nov 30 15:56:19 2010 -0800
@@ -63,7 +63,7 @@
   "match_bind\<cdot>fail\<cdot>k = fail"
   "match_bind\<cdot>(succeed\<cdot>x)\<cdot>k = k\<cdot>x"
 unfolding match_bind_def fail_def succeed_def
-by (simp_all add: cont2cont_Rep_match cont_Abs_match
+by (simp_all add: cont_Rep_match cont_Abs_match
   Rep_match_strict Abs_match_inverse)
 
 subsection {* Case branch combinator *}