diff -r 86c7ed9f354f -r 06e17083e90b Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Wed Dec 23 21:30:23 2009 +0100
+++ b/Quot/quotient_term.ML	Wed Dec 23 22:42:30 2009 +0100
@@ -122,6 +122,15 @@
    for more complicated types of A and B
 *)
 
+(* instantiates TVars so that the term is of type ty *)
+fun force_typ thy trm ty =
+let
+  val trm_ty = fastype_of trm
+  val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty
+in
+  map_types (Envir.subst_type ty_inst) trm
+end
+
 (* builds the aggregate equivalence relation *)
 (* that will be the argument of Respects     *)
 fun mk_resp_arg ctxt (rty, qty) =
@@ -147,15 +156,14 @@
            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; *)
-           (* FIXME: maybe one should actually have a term         *)
-           (* FIXME: and one needs to force it to have this type   *)
+
+           (* we need to instantiate the TVars in the relation *)
+           val thy = ProofContext.theory_of ctxt 
+           val forced_rel = force_typ thy (#rel qinfo) (rty --> rty --> @{typ bool})
          in
-           Const (s, rty --> rty --> @{typ bool})
+           forced_rel
          end
-      | _ => HOLogic.eq_const dummyT 
+      | _ => HOLogic.eq_const rty
              (* FIXME: check that the types correspond to each other? *)
 end