--- a/QuotMain.thy	Thu Oct 15 11:42:14 2009 +0200
+++ b/QuotMain.thy	Thu Oct 15 11:53:11 2009 +0200
@@ -901,7 +901,8 @@
   type needs to respect. *}
 ML {*
 fun tyRel ty rty rel lthy =
-  if ty = rty then rel
+  if ty = rty 
+  then rel
   else (case ty of
           Type (s, tys) =>
             let
@@ -911,10 +912,10 @@
             in
             (case (lookup (ProofContext.theory_of lthy) s) of
                SOME (info) => list_comb (Const (#relfun info, tys_out), map (fn ty => tyRel ty rty rel lthy) tys)
-             | NONE  => Const (@{const_name "op ="}, ty --> ty --> @{typ bool})
+             | NONE  => HOLogic.eq_const ty
             )
             end
-        | _ => Const (@{const_name "op ="}, ty --> ty --> @{typ bool}))
+        | _ => HOLogic.eq_const ty)
 *}
 
 ML {*