--- a/src/HOL/Finite_Set.thy Tue Feb 13 18:26:48 2007 +0100
+++ b/src/HOL/Finite_Set.thy Wed Feb 14 10:06:12 2007 +0100
@@ -2520,7 +2520,7 @@
using hom_Min_commute[of "op + k" N]
apply simp apply(rule arg_cong[where f = Min]) apply blast
apply(simp add:min_def linorder_not_le)
-apply(blast intro:order.antisym order_less_imp_le add_left_mono)
+apply(blast intro:order_class.antisym order_less_imp_le add_left_mono)
done
lemma add_Max_commute: fixes k::"'a::{pordered_ab_semigroup_add,linorder}"
@@ -2529,7 +2529,7 @@
using hom_Max_commute[of "op + k" N]
apply simp apply(rule arg_cong[where f = Max]) apply blast
apply(simp add:max_def linorder_not_le)
-apply(blast intro:order.antisym order_less_imp_le add_left_mono)
+apply(blast intro:order_class.antisym order_less_imp_le add_left_mono)
done