
diff -r 37285ec4387d -r e9e205b904e2 Quot/QuotList.thy
--- a/Quot/QuotList.thy	Sun Dec 20 00:53:35 2009 +0100
+++ b/Quot/QuotList.thy	Mon Dec 21 22:36:31 2009 +0100
@@ -59,7 +59,7 @@
   apply(rule list_rel_rel[OF q])
   done
 
-lemma map_id: "map id \<equiv> id"
+lemma map_id[id_simps]: "map id \<equiv> id"
   apply (rule eq_reflection)
   apply (rule ext)
   apply (rule_tac list="x" in list.induct)




