src/HOL/Tools/Lifting/lifting_def.ML
changeset 47545 a2850a16e30f
parent 47504 aa1b8a59017f
child 47566 c201a1fe0a81
     1.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Wed Apr 18 15:48:32 2012 +0200
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Wed Apr 18 17:04:03 2012 +0200
     1.3 @@ -180,10 +180,9 @@
     1.4      val transfer_thm = [quotient_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer}
     1.5          |> Raw_Simplifier.rewrite_rule (Transfer.get_relator_eq lthy')
     1.6  
     1.7 -    fun qualify defname suffix = Binding.name suffix
     1.8 -      |> Binding.qualify true defname
     1.9 +    fun qualify defname suffix = Binding.qualified true suffix defname
    1.10  
    1.11 -    val lhs_name = Binding.name_of (#1 var)
    1.12 +    val lhs_name = (#1 var)
    1.13      val rsp_thm_name = qualify lhs_name "rsp"
    1.14      val code_eqn_thm_name = qualify lhs_name "rep_eq"
    1.15      val transfer_thm_name = qualify lhs_name "transfer"