# HG changeset patch
# User huffman
# Date 1293071028 28800
# Node ID 17bf4ddd0833d7e8f1501c6c2f442739d7bd9ede
# Parent  d1ff42a70f7714bbc2f7c59e466a7695558dc805
fix another proof script broken by a35af5180c01

diff -r d1ff42a70f77 -r 17bf4ddd0833 src/HOL/HOLCF/Library/Option_Cpo.thy
--- a/src/HOL/HOLCF/Library/Option_Cpo.thy	Wed Dec 22 17:51:22 2010 -0800
+++ b/src/HOL/HOLCF/Library/Option_Cpo.thy	Wed Dec 22 18:23:48 2010 -0800
@@ -265,7 +265,7 @@
   where "option_map f \<equiv> Abs_cfun (Option.map (Rep_cfun f))"
 
 lemma option_map_ID [domain_map_ID]: "option_map ID = ID"
-by (simp add: ID_def cfun_eq_iff Option.map.identity)
+by (simp add: ID_def cfun_eq_iff Option.map.identity id_def)
 
 lemma deflation_option_map [domain_deflation]:
   "deflation d \<Longrightarrow> deflation (option_map d)"