--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/nominal_dt_quot.ML	Sun Jun 27 21:41:21 2010 +0100
@@ -0,0 +1,41 @@
+(*  Title:      nominal_dt_alpha.ML
+    Author:     Christian Urban
+    Author:     Cezary Kaliszyk
+
+  Performing quotient constructions
+*)
+
+signature NOMINAL_DT_QUOT =
+sig
+  val qtype_defs: (string list * binding * mixfix) list -> typ list -> term list -> 
+    thm list -> local_theory -> Quotient_Info.quotdata_info list * local_theory
+
+  val qconst_defs: typ list -> (string  * term * mixfix) list -> local_theory -> 
+    Quotient_Info.qconsts_info list * local_theory
+end
+
+structure Nominal_Dt_Quot: NOMINAL_DT_QUOT =
+struct
+
+(* defines the quotient types *)
+fun qtype_defs qtys_descr alpha_tys alpha_trms alpha_equivp_thms lthy =
+let
+  val qty_args1 = map2 (fn ty => fn trm => (ty, trm, false)) alpha_tys alpha_trms
+  val qty_args2 = (qtys_descr ~~ qty_args1) ~~ alpha_equivp_thms
+in
+  fold_map Quotient_Type.add_quotient_type qty_args2 lthy
+end 
+
+(* defines quotient constants *)
+fun qconst_defs qtys const_spec lthy =
+let
+  val (qconst_infos, lthy') = fold_map (Quotient_Def.lift_raw_const qtys) const_spec lthy
+  val phi = ProofContext.export_morphism lthy' lthy
+in
+  (map (Quotient_Info.transform_qconsts phi) qconst_infos, lthy')
+end
+
+
+
+end (* structure *)
+