--- a/Nominal/Perm.thy	Sat Mar 27 14:38:22 2010 +0100
+++ b/Nominal/Perm.thy	Sat Mar 27 14:55:07 2010 +0100
@@ -9,6 +9,19 @@
 *}
 
 ML {*
+fun quotient_lift_consts_export qtys spec ctxt =
+let
+  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
+  val defs = Morphism.fact morphism defs_loc
+in
+  (ts, defs, ctxt')
+end
+*}
+
+ML {*
 fun prove_perm_empty lthy induct perm_def perm_frees =
 let
   val perm_types = map fastype_of perm_frees;
@@ -118,12 +131,12 @@
 *}
 
 ML {*
-fun define_lifted_perms full_tnames name_term_pairs thms thy =
+fun define_lifted_perms qtys full_tnames name_term_pairs thms thy =
 let
   val lthy =
     Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy;
-  val lthy' = fold (snd oo Quotient_Def.quotient_lift_const) name_term_pairs lthy
-  val lifted_thms = map (fn x => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy', x))) thms
+  val (_, _, lthy') = quotient_lift_consts_export qtys name_term_pairs lthy;
+  val lifted_thms = map (Quotient_Tacs.lifted qtys lthy') thms;
   fun tac _ =
     Class.intro_classes_tac [] THEN
     (ALLGOALS (resolve_tac lifted_thms))