# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1255600653 -7200
# Node ID 3134acbcc42c612ded1a407c83be66eac45cb6d5
# Parent  41a2ab50dd890ba6cadf3963ca876819aaff969f# Parent  9d41f680d755c81a6a427fb7fdbad8cb99609a07
Merged

diff -r 41a2ab50dd89 -r 3134acbcc42c QuotMain.thy
--- a/QuotMain.thy	Thu Oct 15 11:56:30 2009 +0200
+++ b/QuotMain.thy	Thu Oct 15 11:57:33 2009 +0200
@@ -886,7 +886,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
@@ -896,10 +897,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 {*