diff -r de89c95c5377 -r 89f9d7e85e88 Nominal/nominal_dt_quot.ML
--- a/Nominal/nominal_dt_quot.ML	Tue Apr 10 15:22:16 2012 +0100
+++ b/Nominal/nominal_dt_quot.ML	Tue Apr 10 16:02:30 2012 +0100
@@ -64,12 +64,33 @@
     fold_map Quotient_Type.add_quotient_type qty_args3 lthy
   end 
 
+(* a wrapper for lifting a raw constant *)
+fun lift_raw_const qtys (qconst_name, rconst, mx', rsp_thm) lthy =
+  let
+    val rty = fastype_of rconst
+    val qty = Quotient_Term.derive_qtyp lthy qtys rty
+    val lhs_raw = Free (qconst_name, qty)
+    val rhs_raw = rconst
+
+    val raw_var = (Binding.name qconst_name, NONE, mx')
+    val ([(binding, _, mx)], ctxt) = Proof_Context.cert_vars [raw_var] lthy
+    val lhs = Syntax.check_term ctxt lhs_raw
+    val rhs = Syntax.check_term ctxt rhs_raw
+
+    val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."
+    val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"
+    val _ = if is_Const rhs then () else warning "The definiens is not a constant"
+
+  in
+    Quotient_Def.add_quotient_def (((binding, mx), Attrib.empty_binding), (lhs, rhs)) rsp_thm  ctxt
+  end
+
 
 (* defines quotient constants *)
 fun define_qconsts qtys consts_specs lthy =
   let
     val (qconst_infos, lthy') = 
-      fold_map (Quotient_Def.lift_raw_const qtys) consts_specs lthy
+      fold_map (lift_raw_const qtys) consts_specs lthy
     val phi = Proof_Context.export_morphism lthy' lthy
   in
     (map (Quotient_Info.transform_quotconsts phi) qconst_infos, lthy')