diff -r f9bee88c5912 -r df7476e79558 src/HOL/HOLCF/Domain.thy
--- a/src/HOL/HOLCF/Domain.thy	Fri Nov 21 22:59:32 2014 +0100
+++ b/src/HOL/HOLCF/Domain.thy	Sat Nov 22 11:36:00 2014 +0100
@@ -317,7 +317,7 @@
 subsection {* Setting up the domain package *}
 
 named_theorems domain_defl_simps "theorems like DEFL('a t) = t_defl$DEFL('a)"
-named_theorems domain_isodefl "theorems like isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)"
+  and domain_isodefl "theorems like isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)"
 
 ML_file "Tools/Domain/domain_isomorphism.ML"
 ML_file "Tools/Domain/domain_axioms.ML"