diff -r 3045683749af -r 32b67bdf2c3a src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Aug 17 09:20:45 2007 +0200
+++ b/src/HOL/Finite_Set.thy	Fri Aug 17 13:58:57 2007 +0200
@@ -2424,7 +2424,6 @@
   have ne: "{a \<squnion> b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
   have "\<Sqinter>(insert x A) \<squnion> \<Sqinter>B = (x \<sqinter> \<Sqinter>A) \<squnion> \<Sqinter>B"
     using insert
-    thm ACIf.fold1_insert_idem_def
  by(simp add:ACIf.fold1_insert_idem_def[OF ACIf_inf Inf_def])
   also have "\<dots> = (x \<squnion> \<Sqinter>B) \<sqinter> (\<Sqinter>A \<squnion> \<Sqinter>B)" by(rule sup_inf_distrib2)
   also have "\<dots> = \<Sqinter>{x \<squnion> b|b. b \<in> B} \<sqinter> \<Sqinter>{a \<squnion> b|a b. a \<in> A \<and> b \<in> B}"