diff -r c369417be055 -r 0e209ff7f236 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Wed Jul 15 12:44:41 2009 +0200
+++ b/src/HOL/SetInterval.thy	Wed Jul 15 15:09:33 2009 +0200
@@ -425,7 +425,7 @@
 proof cases
   assume "finite A"
   thus "PROP ?P"
-  proof(induct A rule:finite_linorder_induct)
+  proof(induct A rule:finite_linorder_max_induct)
     case empty thus ?case by auto
   next
     case (insert A b)