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