--- a/Nominal/Ex/Lambda.thy	Tue Apr 10 15:21:07 2012 +0100
+++ b/Nominal/Ex/Lambda.thy	Tue Apr 10 15:22:16 2012 +0100
@@ -7,6 +7,8 @@
 
 atom_decl name
 
+ML {* trace := true *}
+
 nominal_datatype lam =
   Var "name"
 | App "lam" "lam"
@@ -19,11 +21,11 @@
 lemma abs_lam_eqvt[eqvt]: "(p \<bullet> abs_lam t) = abs_lam (p \<bullet> t)"
 proof -
   have "alpha_lam_raw (rep_lam (abs_lam t)) t"
-    using rep_abs_rsp_left Quotient_lam equivp_reflp lam_equivp by metis
+    using rep_abs_rsp_left Quotient3_lam equivp_reflp lam_equivp by metis
   then have "alpha_lam_raw (p \<bullet> rep_lam (abs_lam t)) (p \<bullet> t)"
     unfolding alpha_lam_raw_eqvt[symmetric] permute_pure .
   then have "abs_lam (p \<bullet> rep_lam (abs_lam t)) = abs_lam (p \<bullet> t)"
-    using Quotient_rel Quotient_lam by metis
+    using Quotient3_rel Quotient3_lam by metis
   thus ?thesis using permute_lam_def id_apply map_fun_apply by metis
 qed
 

--- a/Nominal/Nominal2.thy	Tue Apr 10 15:21:07 2012 +0100
+++ b/Nominal/Nominal2.thy	Tue Apr 10 15:22:16 2012 +0100
@@ -352,33 +352,38 @@
 
   val _ = trace_msg (K "Defining the quotient constants...")
   val qconstrs_descrs =
-    (map2 o map2) (fn (b, _, mx) => fn t => (Variable.check_name b, t, mx)) (get_cnstrs dts) raw_all_cns
+    (map2 o map2) (fn (b, _, mx) => fn t => (Variable.check_name b, t, mx, @{thm TrueI})) 
+      (get_cnstrs dts) raw_all_cns
 
   val qbns_descr =
-    map2 (fn (b, _, mx) => fn t => (Variable.check_name b, t, mx)) bn_funs raw_bns
+    map2 (fn (b, _, mx) => fn t => (Variable.check_name b, t, mx, @{thm TrueI})) bn_funs raw_bns
 
   val qfvs_descr = 
-    map2 (fn n => fn t => ("fv_" ^ n, t, NoSyn)) qty_names raw_fvs
+    map2 (fn n => fn t => ("fv_" ^ n, t, NoSyn, @{thm TrueI})) qty_names raw_fvs
 
   val qfv_bns_descr = 
-    map2 (fn (b, _, _) => fn t => ("fv_" ^ Variable.check_name b, t, NoSyn)) bn_funs raw_fv_bns
+    map2 (fn (b, _, _) => fn t => ("fv_" ^ Variable.check_name b, t, NoSyn, @{thm TrueI})) 
+      bn_funs raw_fv_bns
 
   val qalpha_bns_descr = 
     let
       val AlphaResult {alpha_bn_trms, ...} = alpha_result 
     in
-      map2 (fn (b, _, _) => fn t => ("alpha_" ^ Variable.check_name b, t, NoSyn)) bn_funs  alpha_bn_trms
+      map2 (fn (b, _, _) => fn t => ("alpha_" ^ Variable.check_name b, t, NoSyn, @{thm TrueI})) 
+        bn_funs  alpha_bn_trms
     end
 
   val qperm_descr =
-    map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn)) qty_names raw_perm_funs
+    map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn, @{thm TrueI})) 
+      qty_names raw_perm_funs
 
   val qsize_descr =
-    map2 (fn n => fn t => ("size_" ^ n, t, NoSyn)) qty_names raw_size_trms
+    map2 (fn n => fn t => ("size_" ^ n, t, NoSyn, @{thm TrueI})) qty_names raw_size_trms
 
   val qperm_bn_descr = 
-    map2 (fn (b, _, _) => fn t => ("permute_" ^ Variable.check_name b, t, NoSyn)) bn_funs raw_perm_bns
-     
+    map2 (fn (b, _, _) => fn t => ("permute_" ^ Variable.check_name b, t, NoSyn, @{thm TrueI})) 
+      bn_funs raw_perm_bns
+
   val ((((((qconstrs_infos, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), qperm_bns_info), 
     lthy8) = 
       lthy7

--- a/Nominal/Nominal2_Abs.thy	Tue Apr 10 15:21:07 2012 +0100
+++ b/Nominal/Nominal2_Abs.thy	Tue Apr 10 15:22:16 2012 +0100
@@ -985,10 +985,10 @@
   by auto
 
 lemma [quot_preserve]:
-  assumes q1: "Quotient R1 abs1 rep1"
-  and     q2: "Quotient R2 abs2 rep2"
+  assumes q1: "Quotient3 R1 abs1 rep1"
+  and     q2: "Quotient3 R2 abs2 rep2"
   shows "((abs1 ---> id) ---> (abs2 ---> id) ---> map_pair rep1 rep2 ---> id) prod_fv = prod_fv"
-  by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
+  by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2])
 
 lemma [mono]: 
   shows "A <= B \<Longrightarrow> C <= D ==> prod_alpha A C <= prod_alpha B D"

--- a/Nominal/nominal_dt_quot.ML	Tue Apr 10 15:21:07 2012 +0100
+++ b/Nominal/nominal_dt_quot.ML	Tue Apr 10 15:22:16 2012 +0100
@@ -11,14 +11,14 @@
   val define_qtypes: (string list * binding * mixfix) list -> typ list -> term list -> 
     thm list -> local_theory -> Quotient_Info.quotients list * local_theory
 
-  val define_qconsts: typ list -> (string  * term * mixfix) list -> local_theory -> 
+  val define_qconsts: typ list -> (string  * term * mixfix * thm) list -> local_theory -> 
     Quotient_Info.quotconsts list * local_theory
 
   val define_qperms: typ list -> string list -> (string * sort) list -> 
-    (string * term * mixfix) list -> thm list -> local_theory -> local_theory
+    (string * term * mixfix * thm) list -> thm list -> local_theory -> local_theory
 
   val define_qsizes: typ list -> string list -> (string * sort) list -> 
-    (string * term * mixfix) list -> local_theory -> local_theory
+    (string * term * mixfix * thm) list -> local_theory -> local_theory
 
   val lift_thms: typ list -> thm list -> thm list -> Proof.context -> thm list * Proof.context