diff -r 77f448727bf9 -r 58e60df1ff79 Nominal/nominal_dt_quot.ML
--- a/Nominal/nominal_dt_quot.ML	Sat Aug 21 20:07:52 2010 +0800
+++ b/Nominal/nominal_dt_quot.ML	Sun Aug 22 11:00:53 2010 +0800
@@ -19,7 +19,7 @@
   val define_qsizes: typ list -> string list -> (string * term * mixfix) list -> 
     local_theory -> local_theory
 
-  val lift_thm: typ list -> Proof.context -> thm -> thm
+  val lift_thm: Proof.context -> typ 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 qtys lthy'') 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,8 @@
   Thm.rename_boundvars trm trm' th
 end
 
-fun lift_thm qtys ctxt thm =
-  Quotient_Tacs.lifted qtys ctxt thm
+fun lift_thm ctxt qtys thm =
+  Quotient_Tacs.lifted ctxt qtys thm
   |> unraw_bounds_thm
   |> unraw_vars_thm