diff -r fff8d328da56 -r cacb00a569e0 src/HOL/HOLCF/Domain_Aux.thy
--- a/src/HOL/HOLCF/Domain_Aux.thy	Fri Aug 15 18:02:34 2014 +0200
+++ b/src/HOL/HOLCF/Domain_Aux.thy	Sat Aug 16 11:35:33 2014 +0200
@@ -344,6 +344,9 @@
 
 subsection {* ML setup *}
 
+named_theorems domain_deflation "theorems like deflation a ==> deflation (foo_map$a)"
+named_theorems domain_map_ID "theorems like foo_map$ID = ID"
+
 ML_file "Tools/Domain/domain_take_proofs.ML"
 ML_file "Tools/cont_consts.ML"
 ML_file "Tools/cont_proc.ML"