--- a/Nominal/Rsp.thy	Sat Aug 21 20:07:52 2010 +0800
+++ b/Nominal/Rsp.thy	Sun Aug 22 11:00:53 2010 +0800
@@ -5,7 +5,7 @@
 ML {*
 fun const_rsp qtys lthy const =
 let
-  val nty = Quotient_Term.derive_qtyp qtys (fastype_of const) lthy
+  val nty = Quotient_Term.derive_qtyp lthy qtys (fastype_of const)
   val rel = Quotient_Term.equiv_relation_chk lthy (fastype_of const, nty);
 in
   HOLogic.mk_Trueprop (rel $ const $ const)