src/HOL/Tools/Quotient/quotient_term.ML
changeset 35402 115a5a95710a
parent 35222 4f1fba00f66d
child 35788 f1deaca15ca3
     1.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Sat Feb 27 20:56:03 2010 +0100
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Sat Feb 27 20:57:08 2010 +0100
     1.3 @@ -265,7 +265,7 @@
     1.4    | is_eq _ = false
     1.5  
     1.6  fun mk_rel_compose (trm1, trm2) =
     1.7 -  Const (@{const_name "rel_conj"}, dummyT) $ trm1 $ trm2
     1.8 +  Const (@{const_abbrev "rel_conj"}, dummyT) $ trm1 $ trm2
     1.9  
    1.10  fun get_relmap ctxt s =
    1.11  let