--- a/Nominal/nominal_dt_quot.ML	Wed Aug 25 11:58:37 2010 +0800
+++ b/Nominal/nominal_dt_quot.ML	Wed Aug 25 20:19:10 2010 +0800
@@ -123,16 +123,11 @@
 end
 
 fun lift_thm ctxt qtys simps thm =
-let
-  val ((_, [thm']), ctxt') = Variable.importT [thm] ctxt
-in
-  thm'
-  |> Quotient_Tacs.lifted ctxt' qtys simps
-  |> singleton (ProofContext.export ctxt' ctxt) 
+  thm
+  |> Quotient_Tacs.lifted ctxt qtys simps
   |> unraw_bounds_thm
   |> unraw_vars_thm
   |> Drule.zero_var_indexes
-end
 
 end (* structure *)