--- a/src/HOL/List.thy Thu Oct 18 14:30:55 2007 +0200
+++ b/src/HOL/List.thy Thu Oct 18 16:09:36 2007 +0200
@@ -2655,9 +2655,7 @@
instance int:: finite_intvl_succ
successor_int_def: "successor == (%i. i+1)"
-apply(intro_classes)
-apply(simp_all add: successor_int_def ord_class.atLeastAtMost[symmetric])
-done
+by intro_classes (simp_all add: successor_int_def)
text{* Now @{term"[i..j::int]"} is defined for integers. *}
--- a/src/HOL/MetisExamples/BigO.thy Thu Oct 18 14:30:55 2007 +0200
+++ b/src/HOL/MetisExamples/BigO.thy Thu Oct 18 16:09:36 2007 +0200
@@ -1145,7 +1145,7 @@
apply (unfold lesso_def)
apply (subgoal_tac "(%x. max (f x - g x) 0) = 0")
(*??Translation of TSTP raised an exception: Type unification failed: Variable ?'X2.0::type not of sort ord*)
-apply (metis bigo_zero ord_class.max)
+apply (metis bigo_zero)
apply (unfold func_zero)
apply (rule ext)
apply (simp split: split_max)