--- 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"