diff -r 4e5bd3883429 -r 557302525778 src/HOL/BNF/Examples/Process.thy
--- a/src/HOL/BNF/Examples/Process.thy	Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Examples/Process.thy	Wed Sep 26 10:00:59 2012 +0200
@@ -45,7 +45,7 @@
 Act: "\<And> a a' p p'. \<phi> (Action a p) (Action a' p') \<Longrightarrow> a = a' \<and> \<phi> p p'" and
 Ch: "\<And> p q p' q'. \<phi> (Choice p q) (Choice p' q') \<Longrightarrow> \<phi> p p' \<and> \<phi> q q'"
 shows "p = p'"
-proof(intro mp[OF process.dtor_rel_coinduct, of \<phi>, OF _ phi], clarify)
+proof(intro mp[OF process.dtor_coinduct, of \<phi>, OF _ phi], clarify)
   fix p p'  assume \<phi>: "\<phi> p p'"
   show "pre_process_rel (op =) \<phi> (process_dtor p) (process_dtor p')"
   proof(cases rule: process.exhaust[of p])