# HG changeset patch
# User huffman
# Date 1293069082 28800
# Node ID d1ff42a70f7714bbc2f7c59e466a7695558dc805
# Parent  b71bcdb568c05c829c000a926f02ea8d8b4f782c
fix proof script broken by a35af5180c01

diff -r b71bcdb568c0 -r d1ff42a70f77 src/HOL/HOLCF/Library/Sum_Cpo.thy
--- a/src/HOL/HOLCF/Library/Sum_Cpo.thy	Wed Dec 22 22:21:14 2010 +0100
+++ b/src/HOL/HOLCF/Library/Sum_Cpo.thy	Wed Dec 22 17:51:22 2010 -0800
@@ -338,7 +338,7 @@
   where "sum_map' f g \<equiv> Abs_cfun (sum_map (Rep_cfun f) (Rep_cfun g))"
 
 lemma sum_map_ID [domain_map_ID]: "sum_map' ID ID = ID"
-by (simp add: ID_def cfun_eq_iff sum_map.identity)
+by (simp add: ID_def cfun_eq_iff sum_map.identity id_def)
 
 lemma deflation_sum_map [domain_deflation]:
   "\<lbrakk>deflation d1; deflation d2\<rbrakk> \<Longrightarrow> deflation (sum_map' d1 d2)"