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