1.1 --- a/src/HOL/Tools/Quotient/quotient_typ.ML	Thu Oct 27 22:20:55 2011 +0200
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Thu Oct 27 22:37:19 2011 +0200
     1.3 @@ -113,8 +113,8 @@
     1.4      val Rep_const = Const (Rep_name, Abs_ty --> Rep_ty)
     1.5  
     1.6      (* more useful abs and rep definitions *)
     1.7 -    val abs_const = Const (@{const_name "quot_type.abs"}, dummyT )
     1.8 -    val rep_const = Const (@{const_name "quot_type.rep"}, dummyT )
     1.9 +    val abs_const = Const (@{const_name quot_type.abs}, dummyT)
    1.10 +    val rep_const = Const (@{const_name quot_type.rep}, dummyT)
    1.11      val abs_trm = Syntax.check_term lthy1 (abs_const $ rel $ Abs_const)
    1.12      val rep_trm = Syntax.check_term lthy1 (rep_const $ Rep_const)
    1.13      val abs_name = Binding.prefix_name "abs_" qty_name