diff -r b29eb13d3f9d -r a746d49b0240 Nominal/nominal_dt_quot.ML
--- a/Nominal/nominal_dt_quot.ML	Sun Aug 22 12:36:53 2010 +0800
+++ b/Nominal/nominal_dt_quot.ML	Sun Aug 22 14:02:49 2010 +0800
@@ -19,7 +19,7 @@
   val define_qsizes: typ list -> string list -> (string * term * mixfix) list -> 
     local_theory -> local_theory
 
-  val lift_thm: Proof.context -> typ list -> thm -> thm
+  val lift_thm: Proof.context -> typ list -> thm list -> thm -> thm
 end
 
 structure Nominal_Dt_Quot: NOMINAL_DT_QUOT =
@@ -56,7 +56,7 @@
   
   val (_, lthy'') = define_qconsts qtys perm_specs lthy'
 
-  val lifted_perm_laws = map (Quotient_Tacs.lifted lthy'' qtys) raw_perm_laws
+  val lifted_perm_laws = map (Quotient_Tacs.lifted lthy'' qtys []) raw_perm_laws
 
   fun tac _ =
     Class.intro_classes_tac [] THEN
@@ -106,8 +106,9 @@
   Thm.rename_boundvars trm trm' th
 end
 
-fun lift_thm ctxt qtys thm =
-  Quotient_Tacs.lifted ctxt qtys thm
+fun lift_thm ctxt qtys simps thm =
+  thm
+  |> Quotient_Tacs.lifted ctxt qtys simps
   |> unraw_bounds_thm
   |> unraw_vars_thm