--- a/Quot/quotient_def.ML	Thu Feb 18 10:01:48 2010 +0100
+++ b/Quot/quotient_def.ML	Thu Feb 18 11:19:16 2010 +0100
@@ -12,6 +12,8 @@
 
   val quotdef_cmd: (binding option * mixfix) * (Attrib.binding * (string * string)) ->
     local_theory -> (term * thm) * local_theory
+
+  val quotient_lift_const: string * term -> local_theory -> (term * thm) * local_theory
 end;
 
 structure Quotient_Def: QUOTIENT_DEF =
@@ -85,6 +87,10 @@
   quotient_def (decl, (attr, (lhs, rhs))) lthy''
 end
 
+fun quotient_lift_const (b, t) ctxt =
+  quotient_def ((NONE, NoSyn), (Attrib.empty_binding,
+    (Quotient_Term.quotient_lift_const (b, t) ctxt, t))) ctxt
+
 local
   structure P = OuterParse;
 in