--- a/src/HOL/Hyperreal/Integration.thy Fri Sep 10 14:54:54 2004 +0200
+++ b/src/HOL/Hyperreal/Integration.thy Fri Sep 10 20:04:14 2004 +0200
@@ -739,9 +739,8 @@
apply (rule partition [THEN iffD2])
apply (frule partition [THEN iffD1])
apply (auto intro: partition_lt_gen)
-apply (drule_tac n = n in partition_lt_gen)
-apply (assumption, arith, blast)
-apply (drule partition_lt_cancel, auto)
+ apply (drule (1) partition_lt_cancel, arith)
+apply (drule (1) partition_lt_cancel, arith)
done
lemma fine_left1: