1.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Fri Oct 28 23:16:50 2011 +0200
     1.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Fri Oct 28 23:41:16 2011 +0200
     1.3 @@ -125,13 +125,13 @@
     1.4  
     1.5  structure DeflMapData = Named_Thms
     1.6  (
     1.7 -  val name = "domain_deflation"
     1.8 +  val name = @{binding domain_deflation}
     1.9    val description = "theorems like deflation a ==> deflation (foo_map$a)"
    1.10  )
    1.11  
    1.12  structure Map_Id_Data = Named_Thms
    1.13  (
    1.14 -  val name = "domain_map_ID"
    1.15 +  val name = @{binding domain_map_ID}
    1.16    val description = "theorems like foo_map$ID = ID"
    1.17  )
    1.18