--- a/Nominal/Perm.thy	Thu Jun 24 21:35:11 2010 +0100
+++ b/Nominal/Perm.thy	Sun Jun 27 21:41:21 2010 +0100
@@ -8,6 +8,7 @@
 uses ("nominal_dt_rawperm.ML")
      ("nominal_dt_rawfuns.ML")
      ("nominal_dt_alpha.ML")
+     ("nominal_dt_quot.ML")
 begin
 
 use "nominal_dt_rawperm.ML"
@@ -19,6 +20,10 @@
 use "nominal_dt_alpha.ML"
 ML {* open Nominal_Dt_Alpha *}
 
+use "nominal_dt_quot.ML"
+ML {* open Nominal_Dt_Quot *}
+
+
 (* permutations for quotient types *)
 
 ML {*
@@ -34,6 +39,8 @@
 end
 *}
 
+
+
 ML {*
 fun define_lifted_perms qtys full_tnames name_term_pairs thms thy =
 let