src/HOL/Complex/ex/NSPrimes.thy

--- a/src/HOL/Complex/ex/NSPrimes.thy	Thu Sep 27 17:28:05 2007 +0200
+++ b/src/HOL/Complex/ex/NSPrimes.thy	Thu Sep 27 17:55:28 2007 +0200
@@ -215,8 +215,7 @@
 apply (rule inj_onI)
 apply (rule ccontr, auto)
 apply (drule injf_max_order_preserving2)
-apply (cut_tac m = x and n = y in less_linear, auto)
-apply (auto dest!: spec)
+apply (metis linorder_antisym_conv3 order_less_le)
 done
 
 lemma infinite_set_has_order_preserving_inj: