# HG changeset patch
# User fleury <Mathias.Fleury@mpi-inf.mpg.de>
# Date 1475670502 -7200
# Node ID 5c2c559f01ebb78ccace859fb07551a925421743
# Parent  c9f3a94cb8258c80a6fa5109ddd3bc7ba979d669
tuned proof -- much faster

diff -r c9f3a94cb825 -r 5c2c559f01eb src/HOL/Cardinals/Ordinal_Arithmetic.thy
--- a/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Mon Oct 03 14:37:06 2016 +0200
+++ b/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Wed Oct 05 14:28:22 2016 +0200
@@ -1660,7 +1660,7 @@
     thus "((x, y), (s.max_fun_diff (rev_curr f m) (rev_curr g m), m)) \<in> s *o t"
       using rst.max_fun_diff_in[OF diff1] rs.max_fun_diff_in[OF diff2] diff1 diff2
         rst.max_fun_diff_max[OF diff1, of y] rs.max_fun_diff_le_eq[OF _ diff2, of x]
-      unfolding oprod_def m_def rev_curr_def fun_eq_iff by auto (metis s.in_notinI)
+      unfolding oprod_def m_def rev_curr_def fun_eq_iff by (auto intro: s.in_notinI)
   qed
 qed