# HG changeset patch
# User haftmann
# Date 1238152921 -3600
# Node ID 3e89ac3905b9b837249670d0a73985a087af34f1
# Parent  9e23e3ea7eddb6603edd576f21cf7dc477a0de6c
tuned notoriously slow metis proof

diff -r 9e23e3ea7edd -r 3e89ac3905b9 src/HOL/Library/Permutation.thy
--- a/src/HOL/Library/Permutation.thy	Fri Mar 27 10:12:55 2009 +0100
+++ b/src/HOL/Library/Permutation.thy	Fri Mar 27 12:22:01 2009 +0100
@@ -188,7 +188,11 @@
    apply (subgoal_tac "set (a#list) = set (ysa@a#zs) & distinct (a#list) & distinct (ysa@a#zs)")
     apply (fastsimp simp add: insert_ident)
    apply (metis distinct_remdups set_remdups)
-  apply (metis le_less_trans Suc_length_conv length_remdups_leq less_Suc_eq nat_less_le)
+   apply (subgoal_tac "length (remdups xs) < Suc (length xs)")
+   apply simp
+   apply (subgoal_tac "length (remdups xs) \<le> length xs")
+   apply simp
+   apply (rule length_remdups_leq)
   done
 
 lemma perm_remdups_iff_eq_set: "remdups x <~~> remdups y = (set x = set y)"