diff -r 0d10196364aa -r 558c823f96aa Nominal/Perm.thy
--- a/Nominal/Perm.thy	Thu Jun 24 00:41:41 2010 +0100
+++ b/Nominal/Perm.thy	Thu Jun 24 19:32:33 2010 +0100
@@ -24,8 +24,8 @@
 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 (result, ctxt') = fold_map (Quotient_Def.lift_raw_const qtys) spec ctxt;
+  val (ts_loc, defs_loc) = split_list (map (fn info => (#qconst info, #def info)) result);
   val morphism = ProofContext.export_morphism ctxt' ctxt;
   val ts = map (Morphism.term morphism) ts_loc
   val defs = Morphism.fact morphism defs_loc