
diff -r 2480fb2a5e4e -r 5961edda27d7 Quot/Examples/FSet3.thy
--- a/Quot/Examples/FSet3.thy	Tue Jan 12 10:59:51 2010 +0100
+++ b/Quot/Examples/FSet3.thy	Wed Jan 13 00:45:28 2010 +0100
@@ -369,8 +369,6 @@
 apply(cleaning)
 apply (simp add: finsert_def fconcat_def comp_def)
 apply cleaning
-(* ID PROBLEM *)
-apply(simp add: id_def[symmetric] id_simps)
 done
 
 text {* raw section *}




