src/HOLCF/Fixrec.thy
changeset 16754 1b979f8b7e8e
parent 16551 7abf8a713613
child 16758 c32334d98fcd
--- a/src/HOLCF/Fixrec.thy	Fri Jul 08 02:41:19 2005 +0200
+++ b/src/HOLCF/Fixrec.thy	Fri Jul 08 02:41:35 2005 +0200
@@ -26,7 +26,7 @@
 apply (unfold fail_def return_def)
 apply (rule_tac p=p in ssumE, simp)
 apply (rule_tac p=x in oneE, simp, simp)
-apply (rule_tac p=y in upE1, simp, simp)
+apply (rule_tac p=y in upE, simp, simp)
 done
 
 subsection {* Monadic bind operator *}