# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1282738750 -28800
# Node ID ff887850d83c48caa1cb3a4aa36a6119b89f0de4
# Parent  7aa18bae69839384cfb1510fdd905e83d6c24726
everything now lifts as expected

diff -r 7aa18bae6983 -r ff887850d83c Nominal/nominal_dt_quot.ML
--- 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 *)