--- a/Nominal/Lift.thy	Sat Aug 21 17:55:42 2010 +0800
+++ b/Nominal/Lift.thy	Sat Aug 21 20:07:36 2010 +0800
@@ -18,49 +18,42 @@
 end
 *}
 
-(* Renames schematic variables in a theorem *)
+(* Unrawifying schematic and bound variables *)
+
 ML {*
-fun rename_vars fnctn thm =
+fun unraw_str s = 
+  unsuffix "_raw" s
+  handle Fail _ => s
+
+fun unraw_vars_thm thm =
 let
+  fun unraw_var ((s, i), T) = ((unraw_str s, i), T)
+
   val vars = Term.add_vars (prop_of thm) []
-  val nvars = map (Var o ((apfst o apfst) fnctn)) vars
+  val nvars = map (Var o unraw_var) vars
 in
   Thm.certify_instantiate ([], (vars ~~ nvars))  thm
 end
 *}
 
 ML {*
-fun un_raws name =
+fun unraw_bounds_thm th =
 let
-  fun un_raw name = unprefix "_raw" name handle Fail _ => name
-  fun add_under names = hd names :: (map (prefix "_") (tl names))
+  val trm = Thm.prop_of th
+  val trm' = Term.map_abs_vars unraw_str trm
 in
-  implode (map un_raw (add_under (space_explode "_" name)))
+  Thm.rename_boundvars trm trm' th
 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 qtys ctxt thm =
-let
-  val un_raw_names = rename_vars un_raws
-in
-  rename_thm_bvars (un_raw_names (Quotient_Tacs.lifted qtys ctxt thm))
-end
+  Quotient_Tacs.lifted qtys ctxt thm
+  |> unraw_bounds_thm
+  |> unraw_vars_thm
 *}
 
+
 end