--- a/QuotMain.thy	Mon Nov 23 21:12:16 2009 +0100
+++ b/QuotMain.thy	Mon Nov 23 21:48:44 2009 +0100
@@ -1264,7 +1264,7 @@
        in
          if ty = ty'
          then Const (@{const_name "op ="}, ty) $ subtrm
-         else mk_resp_arg lthy (ty, ty') $ subtrm
+         else mk_resp_arg lthy (domain_type ty, domain_type ty') $ subtrm
        end 
   | (t1 $ t2, t1' $ t2') =>
        (REGULARIZE_trm lthy t1 t1') $ (REGULARIZE_trm lthy t2 t2')