--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Oct 28 23:16:50 2011 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Oct 28 23:41:16 2011 +0200
@@ -46,13 +46,13 @@
structure RepData = Named_Thms
(
- val name = "domain_defl_simps"
+ val name = @{binding domain_defl_simps}
val description = "theorems like DEFL('a t) = t_defl$DEFL('a)"
)
structure IsodeflData = Named_Thms
(
- val name = "domain_isodefl"
+ val name = @{binding domain_isodefl}
val description = "theorems like isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)"
)