diff -r 1c9931e5039a -r 2ff84b1f551f Nominal/Lift.thy
--- a/Nominal/Lift.thy	Thu Mar 18 08:03:42 2010 +0100
+++ b/Nominal/Lift.thy	Thu Mar 18 08:32:55 2010 +0100
@@ -3,14 +3,45 @@
 begin
 
 ML {*
-fun lift_thm ctxt thm =
+fun rename_vars fnctn thm =
+let
+  val vars = Term.add_vars (prop_of thm) []
+  val nvars = map (Var o ((apfst o apfst) fnctn)) vars
+in
+  Thm.certify_instantiate ([], (vars ~~ nvars))  thm
+end
+*}
+
+ML {*
+fun un_raws name =
 let
   fun un_raw name = unprefix "_raw" name handle Fail _ => name
   fun add_under names = hd names :: (map (prefix "_") (tl names))
-  fun un_raws name = implode (map un_raw (add_under (space_explode "_" name)))
+in
+  implode (map un_raw (add_under (space_explode "_" name)))
+end
+*}
+
+(* Similar to Tools/IsaPlanner/rw_tools.ML *)
+ML {*
+fun rename_term_bvars (Abs(s, ty, t)) = (Abs(un_raws s, ty, rename_term_bvars t))
+  | rename_term_bvars (a $ b) = (rename_term_bvars a) $ (rename_term_bvars b)
+  | rename_term_bvars x = x;
+
+fun rename_thm_bvars th =
+let
+  val t = Thm.prop_of th
+in
+  Thm.rename_boundvars t (rename_term_bvars t) th
+end;
+*}
+
+ML {*
+fun lift_thm ctxt thm =
+let
   val un_raw_names = rename_vars un_raws
 in
-  un_raw_names (snd (Quotient_Tacs.lifted_attrib (Context.Proof ctxt, thm)))
+  rename_thm_bvars (un_raw_names (snd (Quotient_Tacs.lifted_attrib (Context.Proof ctxt, thm))))
 end
 *}