src/HOL/BNF/Examples/TreeFI.thy

--- a/src/HOL/BNF/Examples/TreeFI.thy	Wed Apr 24 17:03:43 2013 +0200
+++ b/src/HOL/BNF/Examples/TreeFI.thy	Wed Apr 24 17:47:22 2013 +0200
@@ -16,7 +16,7 @@
 
 lemma pre_treeFI_listF_set[simp]: "pre_treeFI_set2 (i, xs) = listF_set xs"
 unfolding pre_treeFI_set2_def collect_def[abs_def] prod_set_defs
-by (auto simp add: listF.set_natural')
+by (auto simp add: listF.set_map')
 
 lemma dtor[simp]: "treeFI_dtor tr = (lab tr, sub tr)"
 unfolding lab_def sub_def treeFI_case_def