diff -r ae54ce4cde54 -r f78c820f67c3 Nominal/Lift.thy
--- a/Nominal/Lift.thy	Sat Mar 27 14:38:22 2010 +0100
+++ b/Nominal/Lift.thy	Sat Mar 27 14:55:07 2010 +0100
@@ -55,18 +55,18 @@
 *}
 
 ML {*
-fun lift_thm ctxt thm =
+fun lift_thm qtys ctxt thm =
 let
   val un_raw_names = rename_vars un_raws
 in
-  rename_thm_bvars (un_raw_names (snd (Quotient_Tacs.lifted_attrib (Context.Proof ctxt, thm))))
+  rename_thm_bvars (un_raw_names (Quotient_Tacs.lifted qtys ctxt thm))
 end
 *}
 
 ML {*
-fun quotient_lift_consts_export spec ctxt =
+fun quotient_lift_consts_export qtys spec ctxt =
 let
-  val (result, ctxt') = fold_map Quotient_Def.quotient_lift_const spec ctxt;
+  val (result, ctxt') = fold_map (Quotient_Def.quotient_lift_const qtys) spec ctxt;
   val (ts_loc, defs_loc) = split_list result;
   val morphism = ProofContext.export_morphism ctxt' ctxt;
   val ts = map (Morphism.term morphism) ts_loc