--- a/Nominal/Lift.thy	Sat Mar 27 16:17:45 2010 +0100
+++ b/Nominal/Lift.thy	Sat Mar 27 16:20:39 2010 +0100
@@ -64,19 +64,6 @@
 *}
 
 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 define_fv_alpha_export dt binds bns ctxt =
 let
   val ((((fv_ts_loc, fv_def_loc), ord_fv_ts_loc), alpha), ctxt') =