--- a/Nominal/Rsp.thy	Thu Jun 24 00:41:41 2010 +0100
+++ b/Nominal/Rsp.thy	Thu Jun 24 19:32:33 2010 +0100
@@ -5,7 +5,7 @@
 ML {*
 fun const_rsp qtys lthy const =
 let
-  val nty = fastype_of (Quotient_Term.quotient_lift_const qtys ("", const) lthy)
+  val nty = Quotient_Term.derive_qtyp qtys (fastype_of const) lthy
   val rel = Quotient_Term.equiv_relation_chk lthy (fastype_of const, nty);
 in
   HOLogic.mk_Trueprop (rel $ const $ const)