--- a/Nominal/nominal_dt_quot.ML	Wed Aug 25 20:19:10 2010 +0800
+++ b/Nominal/nominal_dt_quot.ML	Wed Aug 25 22:55:42 2010 +0800
@@ -19,7 +19,7 @@
   val define_qsizes: typ list -> string list -> (string * sort) list -> 
     (string * term * mixfix) list -> local_theory -> local_theory
 
-  val lift_thm: Proof.context -> typ list -> thm list -> thm -> thm
+  val lift_thms: typ list -> thm list -> thm list -> Proof.context -> thm list * Proof.context
 end
 
 structure Nominal_Dt_Quot: NOMINAL_DT_QUOT =
@@ -49,8 +49,6 @@
 (* defines the quotient permutations and proves pt-class *)
 fun define_qperms qtys qfull_ty_names tvs perm_specs raw_perm_laws lthy =
 let
-  val _ = tracing ("qtys:\n" ^ cat_lines (map @{make_string} qtys))
-
   val lthy1 = 
     lthy
     |> Local_Theory.exit_global
@@ -122,12 +120,12 @@
   Thm.rename_boundvars trm trm' th
 end
 
-fun lift_thm ctxt qtys simps thm =
-  thm
-  |> Quotient_Tacs.lifted ctxt qtys simps
-  |> unraw_bounds_thm
-  |> unraw_vars_thm
-  |> Drule.zero_var_indexes
+fun lift_thms qtys simps thms ctxt =
+  (map (Quotient_Tacs.lifted ctxt qtys simps
+        #> unraw_bounds_thm
+        #> unraw_vars_thm
+        #> Drule.zero_var_indexes) thms, ctxt)
+
 
 end (* structure *)