diff -r 7851e2a74f85 -r 5a7024be9083 QuotMain.thy
--- a/QuotMain.thy	Mon Nov 23 10:26:59 2009 +0100
+++ b/QuotMain.thy	Mon Nov 23 13:24:12 2009 +0100
@@ -1212,10 +1212,16 @@
 let
   val thy = ProofContext.theory_of lthy
 in  
-  case (rty, qty) of
-    (Type (s, tys), Type (s', tys')) =>
+  if rty = qty
+  then HOLogic.eq_const rty
+  else
+    case (rty, qty) of
+      (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
@@ -1228,7 +1234,7 @@
             in
               #rel qinfo
             end
-    | _ => HOLogic.eq_const dummyT 
+      | _ => HOLogic.eq_const dummyT 
            (* FIXME: do the types correspond to each other? *)
 end
 *}
@@ -1263,7 +1269,7 @@
   | _ => f trm1 trm2
 
 (* the major type of All and Ex quantifiers *)
-fun qnt_typ ty = domain_type (domain_type ty)
+fun qnt_typ ty = domain_type (domain_type ty)  
 *}
 
 (*
@@ -1305,6 +1311,9 @@
   | (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
@@ -1313,12 +1322,15 @@
   | (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
          else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm
        end
-  (* FIXME: Why is there a case for equality? Is it correct? *)
+    (* FIXME: should be replaced when fully applied? then 2nd argument *)
   | (Const (@{const_name "op ="}, ty) $ t, Const (@{const_name "op ="}, ty') $ t') =>
        let
          val subtrm = REGULARIZE_trm lthy t t'