src/HOL/Library/Mapping.thy
changeset 33640 0d82107dc07a
parent 31459 ae39b7b2a68a
child 35157 73cd6f78c86d
--- a/src/HOL/Library/Mapping.thy	Thu Nov 12 17:21:48 2009 +0100
+++ b/src/HOL/Library/Mapping.thy	Thu Nov 12 17:21:51 2009 +0100
@@ -128,7 +128,7 @@
 lemma bulkload_tabulate:
   "bulkload xs = tabulate [0..<length xs] (nth xs)"
   by (rule sym)
-    (auto simp add: bulkload_def tabulate_def expand_fun_eq map_of_eq_None_iff map_compose [symmetric] comp_def)
+    (auto simp add: bulkload_def tabulate_def expand_fun_eq map_of_eq_None_iff comp_def)
 
 
 subsection {* Some technical code lemmas *}