diff -r 45fb38a2e3f7 -r 61671de8a545 Attic/Quot/quotient_term.ML
--- a/Attic/Quot/quotient_term.ML	Sun Mar 14 11:36:15 2010 +0100
+++ b/Attic/Quot/quotient_term.ML	Mon Mar 15 06:11:35 2010 +0100
@@ -1,8 +1,8 @@
-(*  Title:      quotient_term.thy
+(*  Title:      HOL/Tools/Quotient/quotient_term.thy
     Author:     Cezary Kaliszyk and Christian Urban
 
-    Constructs terms corresponding to goals from
-    lifting theorems to quotient types.
+Constructs terms corresponding to goals from lifting theorems to
+quotient types.
 *)
 
 signature QUOTIENT_TERM =
@@ -265,7 +265,7 @@
   | is_eq _ = false
 
 fun mk_rel_compose (trm1, trm2) =
-  Const (@{const_name "rel_conj"}, dummyT) $ trm1 $ trm2
+  Const (@{const_abbrev "rel_conj"}, dummyT) $ trm1 $ trm2
 
 fun get_relmap ctxt s =
 let
@@ -779,8 +779,4 @@
   lift_aux t
 end
 
-
 end; (* structure *)
-
-
-