--- a/QuotMain.thy	Mon Nov 23 22:00:54 2009 +0100
+++ b/QuotMain.thy	Mon Nov 23 23:09:03 2009 +0100
@@ -1146,9 +1146,6 @@
       (Type (s, tys), Type (s', tys')) =>
        if s = s' 
        then let
-              val _ = tracing ("maps lookup for  " ^ s)
-              val _ = tracing (Syntax.string_of_typ lthy rty)
-              val _ = tracing (Syntax.string_of_typ lthy qty)
               val SOME map_info = maps_lookup thy s
               val args = map (mk_resp_arg lthy) (tys ~~ tys')
             in
@@ -1158,8 +1155,11 @@
               val SOME qinfo = quotdata_lookup_thy thy s'
               (* FIXME: check in this case that the rty and qty *)
               (* FIXME: correspond to each other *)
+              val (s, _) = dest_Const (#rel qinfo)
+              (* FIXME: the relation should only be the string       *)
+              (* FIXME: and the type needs to be calculated as below *) 
             in
-              #rel qinfo
+              Const (s, rty --> rty --> @{typ bool})
             end
       | _ => HOLogic.eq_const dummyT 
              (* FIXME: check that the types correspond to each other? *)
@@ -1238,9 +1238,6 @@
   | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
        let
          val subtrm = apply_subt (REGULARIZE_trm lthy) t t'
-         val _ = tracing "quantor types All"
-         val _ = tracing (Syntax.string_of_typ lthy ty)
-         val _ = tracing (Syntax.string_of_typ lthy ty')
        in
          if ty = ty'
          then Const (@{const_name "All"}, ty) $ subtrm
@@ -1249,9 +1246,6 @@
   | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
        let
          val subtrm = apply_subt (REGULARIZE_trm lthy) t t'
-         val _ = tracing "quantor types Ex"
-         val _ = tracing (Syntax.string_of_typ lthy ty)
-         val _ = tracing (Syntax.string_of_typ lthy ty')
        in
          if ty = ty'
          then Const (@{const_name "Ex"}, ty) $ subtrm