src/ZF/Induct/Tree_Forest.thy

--- a/src/ZF/Induct/Tree_Forest.thy	Sun Jun 24 11:41:41 2018 +0100
+++ b/src/ZF/Induct/Tree_Forest.thy	Sun Jun 24 15:57:48 2018 +0200
@@ -245,7 +245,7 @@
 \<close>
 
 lemma preorder_map:
-    "z \<in> tree_forest(A) ==> preorder(map(h,z)) = List_ZF.map(h, preorder(z))"
+    "z \<in> tree_forest(A) ==> preorder(map(h,z)) = List.map(h, preorder(z))"
   by (induct set: tree_forest) (simp_all add: map_app_distrib)
 
 end