--- a/Nominal/nominal_dt_quot.ML	Sun Aug 15 11:03:13 2010 +0800
+++ b/Nominal/nominal_dt_quot.ML	Sun Aug 15 14:00:28 2010 +0800
@@ -7,21 +7,24 @@
 
 signature NOMINAL_DT_QUOT =
 sig
-  val qtype_defs: (string list * binding * mixfix) list -> typ list -> term list -> 
+  val define_qtypes: (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 -> 
+  val define_qconsts: typ list -> (string  * term * mixfix) list -> local_theory -> 
     Quotient_Info.qconsts_info list * local_theory
 
-  val qperm_defs: typ list -> string list -> (string * term * mixfix) list -> 
+  val define_qperms: typ list -> string list -> (string * term * mixfix) list -> 
     thm list -> theory -> theory
+
+  val define_qsizes: typ list -> string list -> (string * term * mixfix) list -> 
+    theory -> 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 =
+fun define_qtypes 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
@@ -31,7 +34,7 @@
 
 
 (* defines quotient constants *)
-fun qconst_defs qtys consts_specs lthy =
+fun define_qconsts qtys consts_specs lthy =
 let
   val (qconst_infos, lthy') = 
     fold_map (Quotient_Def.lift_raw_const qtys) consts_specs lthy
@@ -41,24 +44,36 @@
 end
 
 
-(* defines the quotient permutations *)
-fun qperm_defs qtys full_tnames perm_specs thms thy =
+(* defines the quotient permutations and proves pt-class *)
+fun define_qperms qtys qfull_ty_names perm_specs raw_perm_laws thy =
 let
-  val lthy =
-    Class.instantiation (full_tnames, [], @{sort pt}) thy;
+  val lthy = Class.instantiation (qfull_ty_names, [], @{sort pt}) thy
   
-  val (_, lthy') = qconst_defs qtys perm_specs lthy;
+  val (_, lthy') = define_qconsts qtys perm_specs lthy
 
-  val lifted_thms = map (Quotient_Tacs.lifted qtys lthy') thms;
+  val lifted_perm_laws = map (Quotient_Tacs.lifted qtys lthy') raw_perm_laws
 
   fun tac _ =
     Class.intro_classes_tac [] THEN
-      (ALLGOALS (resolve_tac lifted_thms))
+      (ALLGOALS (resolve_tac lifted_perm_laws))
 in
   lthy'
   |> Class.prove_instantiation_exit tac 
 end
 
 
+(* defines the size functions and proves size-class *)
+fun define_qsizes qtys qfull_ty_names size_specs thy =
+let
+  val lthy = Class.instantiation (qfull_ty_names, [], @{sort size}) thy
+  
+  val (_, lthy') = define_qconsts qtys size_specs lthy
+
+  fun tac _ = Class.intro_classes_tac []
+in
+  lthy'
+  |> Class.prove_instantiation_exit tac
+end
+
 end (* structure *)