--- a/Quot/quotient_term.ML	Thu Feb 18 23:07:28 2010 +0100
+++ b/Quot/quotient_term.ML	Thu Feb 18 23:07:52 2010 +0100
@@ -26,6 +26,7 @@
   val inj_repabs_trm: Proof.context -> term * term -> term
   val inj_repabs_trm_chk: Proof.context -> term * term -> term
 
+  val quotient_lift_const: string * term -> local_theory -> term
   val quotient_lift_all: Proof.context -> term -> term
 end;
 
@@ -732,6 +733,15 @@
   (ty_substs, const_substs @ rel_substs)
 end
 
+fun quotient_lift_const (b, t) ctxt =
+let
+  val thy = ProofContext.theory_of ctxt
+  val (ty_substs, _) = get_ty_trm_substs ctxt;
+  val (_, ty) = dest_Const t;
+  val nty = subst_tys thy ty_substs ty;
+in
+  Free(b, nty)
+end
 
 (*
 Takes a term and