diff -r 80e2fb39332b -r de89c95c5377 Nominal/nominal_dt_quot.ML
--- 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