diff -r b151399bd2c3 -r e1764a73c292 Nominal/nominal_dt_quot.ML
--- a/Nominal/nominal_dt_quot.ML	Sun Jun 27 21:41:21 2010 +0100
+++ b/Nominal/nominal_dt_quot.ML	Mon Jun 28 15:23:56 2010 +0100
@@ -26,10 +26,12 @@
   fold_map Quotient_Type.add_quotient_type qty_args2 lthy
 end 
 
+
 (* defines quotient constants *)
-fun qconst_defs qtys const_spec lthy =
+fun qconst_defs qtys consts_specs lthy =
 let
-  val (qconst_infos, lthy') = fold_map (Quotient_Def.lift_raw_const qtys) const_spec lthy
+  val (qconst_infos, lthy') = 
+    fold_map (Quotient_Def.lift_raw_const qtys) consts_specs lthy
   val phi = ProofContext.export_morphism lthy' lthy
 in
   (map (Quotient_Info.transform_qconsts phi) qconst_infos, lthy')