--- a/Nominal/nominal_dt_quot.ML	Fri Jul 02 15:34:46 2010 +0100
+++ b/Nominal/nominal_dt_quot.ML	Wed Jul 07 09:34:00 2010 +0100
@@ -12,6 +12,9 @@
 
   val qconst_defs: 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 -> 
+    thm list -> theory -> theory
 end
 
 structure Nominal_Dt_Quot: NOMINAL_DT_QUOT =
@@ -38,6 +41,21 @@
 end
 
 
+(* defines the quotient permutations *)
+fun qperm_defs qtys full_tnames name_term_pairs thms thy =
+let
+  val lthy =
+    Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy;
+  val (_, lthy') = qconst_defs qtys name_term_pairs lthy;
+  val lifted_thms = map (Quotient_Tacs.lifted qtys lthy') thms;
+  fun tac _ =
+    Class.intro_classes_tac [] THEN
+    (ALLGOALS (resolve_tac lifted_thms))
+  val lthy'' = Class.prove_instantiation_instance tac lthy'
+in
+  Local_Theory.exit_global lthy''
+end
+
 
 end (* structure *)