# HG changeset patch
# User blanchet
# Date 1377808786 -7200
# Node ID 7422380afe235e26dda85c9f16862ef563d629d3
# Parent  f096456429848e00ae19fcd2d17c17926a4f382d
compile

diff -r f09645642984 -r 7422380afe23 src/HOL/BNF/More_BNFs.thy
--- a/src/HOL/BNF/More_BNFs.thy	Thu Aug 29 22:39:46 2013 +0200
+++ b/src/HOL/BNF/More_BNFs.thy	Thu Aug 29 22:39:46 2013 +0200
@@ -227,7 +227,7 @@
 apply transfer apply simp
 done
 
-lemmas [simp] = fset.map_comp' fset.map_id' fset.set_map'
+lemmas [simp] = fset.map_comp' fset.map_id fset.set_map'
 
 lemma fset_rel_fset: "set_rel \<chi> (fset A1) (fset A2) = fset_rel \<chi> A1 A2"
   unfolding fset_rel_def set_rel_def by auto