src/HOL/BNF_Examples/TreeFsetI.thy
changeset 55933 12ee2c407dad
parent 55129 26bd1cba3ab5
--- a/src/HOL/BNF_Examples/TreeFsetI.thy	Thu Mar 06 13:36:48 2014 +0100
+++ b/src/HOL/BNF_Examples/TreeFsetI.thy	Thu Mar 06 13:36:49 2014 +0100
@@ -20,6 +20,6 @@
 "sub (tmap f t) = fimage (tmap f) (sub t)"
 
 lemma "tmap (f o g) x = tmap f (tmap g x)"
-  by (coinduction arbitrary: x) (auto simp: fset_rel_alt)
+  by (coinduction arbitrary: x) (auto simp: rel_fset_alt)
 
 end