--- a/Nominal/Rsp.thy	Sat Mar 27 14:38:22 2010 +0100
+++ b/Nominal/Rsp.thy	Sat Mar 27 14:55:07 2010 +0100
@@ -3,9 +3,9 @@
 begin
 
 ML {*
-fun const_rsp lthy const =
+fun const_rsp qtys lthy const =
 let
-  val nty = fastype_of (Quotient_Term.quotient_lift_const ("", const) lthy)
+  val nty = fastype_of (Quotient_Term.quotient_lift_const qtys ("", const) lthy)
   val rel = Quotient_Term.equiv_relation_chk lthy (fastype_of const, nty);
 in
   HOLogic.mk_Trueprop (rel $ const $ const)
@@ -39,9 +39,9 @@
 *}
 
 ML {*
-fun prove_const_rsp bind consts tac ctxt =
+fun prove_const_rsp qtys bind consts tac ctxt =
 let
-  val rsp_goals = map (const_rsp ctxt) consts
+  val rsp_goals = map (const_rsp qtys ctxt) consts
   val thy = ProofContext.theory_of ctxt
   val (fixed, user_goals) = split_list (map (get_rsp_goal thy) rsp_goals)
   val fixed' = distinct (op =) (flat fixed)