
diff -r a9a002f4b715 -r e9de8d69c1b9 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Wed Nov 04 09:18:46 2009 +0100
+++ b/src/HOL/SetInterval.thy	Wed Nov 04 10:17:43 2009 +0100
@@ -508,7 +508,7 @@
   proof(induct A rule:finite_linorder_max_induct)
     case empty thus ?case by auto
   next
-    case (insert A b)
+    case (insert b A)
     moreover hence "b ~: A" by auto
     moreover have "A <= {k..<k+card A}" and "b = k+card A"
       using `b ~: A` insert by fastsimp+




