# HG changeset patch
# User nipkow
# Date 1525611492 -7200
# Node ID 152cc388cd1ee23f91cad2a4d18bdbaac467d961
# Parent  d730a8cfc6e0466deced2cd085e521b882e628cf
updated to lemma name change

diff -r d730a8cfc6e0 -r 152cc388cd1e src/HOL/ex/Perm_Fragments.thy
--- a/src/HOL/ex/Perm_Fragments.thy	Sun May 06 13:51:37 2018 +0200
+++ b/src/HOL/ex/Perm_Fragments.thy	Sun May 06 14:58:12 2018 +0200
@@ -266,7 +266,7 @@
   have "set.F h (set (sorted_list_of_set A)) = list.F (map h (sorted_list_of_set A))"
     by (rule distinct_set_conv_list)
   with \<open>finite A\<close> show ?thesis
-    by (simp add: sorted_list_of_set)
+    by (simp)
 qed