# HG changeset patch
# User wenzelm
# Date 1319747839 -7200
# Node ID 9e8616978d9956d9150cd0440b0fb2f3e47f6d8e
# Parent  eaec1651709ab332a5e99cc38a863829ac9bc381
tuned;

diff -r eaec1651709a -r 9e8616978d99 src/HOL/Tools/Quotient/quotient_typ.ML
--- a/src/HOL/Tools/Quotient/quotient_typ.ML	Thu Oct 27 22:20:55 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Thu Oct 27 22:37:19 2011 +0200
@@ -113,8 +113,8 @@
     val Rep_const = Const (Rep_name, Abs_ty --> Rep_ty)
 
     (* more useful abs and rep definitions *)
-    val abs_const = Const (@{const_name "quot_type.abs"}, dummyT )
-    val rep_const = Const (@{const_name "quot_type.rep"}, dummyT )
+    val abs_const = Const (@{const_name quot_type.abs}, dummyT)
+    val rep_const = Const (@{const_name quot_type.rep}, dummyT)
     val abs_trm = Syntax.check_term lthy1 (abs_const $ rel $ Abs_const)
     val rep_trm = Syntax.check_term lthy1 (rep_const $ Rep_const)
     val abs_name = Binding.prefix_name "abs_" qty_name