--- a/Nominal/Fv.thy	Thu Mar 11 14:09:54 2010 +0100
+++ b/Nominal/Fv.thy	Thu Mar 11 15:11:57 2010 +0100
@@ -696,4 +696,14 @@
       | SOME i => i
 *}
 
+ML {*
+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
+*}
+
+end

--- a/Nominal/Parser.thy	Thu Mar 11 14:09:54 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 11 15:11:57 2010 +0100
@@ -253,7 +253,13 @@
 end
 *}
 
-ML {* add_primrec_wrapper *}
+ML {*
+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)))
+val un_raw_names = rename_vars un_raws
+fun lift_thm ctxt thm = un_raw_names (snd (Quotient_Tacs.lifted_attrib (Context.Proof ctxt, thm)))
+*}
 
 lemma equivp_hack: "equivp x"
 sorry
@@ -381,23 +387,23 @@
   val thy' = define_lifted_perms qty_full_names (perm_names ~~ perms) raw_perm_simps thy;
   val lthy13 = Theory_Target.init NONE thy';
   val q_name = space_implode "_" qty_names;
-  val q_induct = snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy13, induct));
+  val q_induct = lift_thm lthy13 induct;
   val (_, lthy14) = Local_Theory.note ((Binding.name (q_name ^ "_induct"), []), [q_induct]) lthy13;
-  val q_perm = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy14, th))) raw_perm_def;
+  val q_perm = map (lift_thm lthy14) raw_perm_def;
   val (_, lthy15) = Local_Theory.note ((Binding.name (q_name ^ "_perm"), []), q_perm) lthy14;
-  val q_fv = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy15, th))) fv_def;
+  val q_fv = map (lift_thm lthy15) fv_def;
   val (_, lthy16) = Local_Theory.note ((Binding.name (q_name ^ "_fv"), []), q_fv) lthy15;
-  val q_bn = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy16, th))) raw_bn_eqs;
+  val q_bn = map (lift_thm lthy16) raw_bn_eqs;
   val (_, lthy17) = Local_Theory.note ((Binding.name (q_name ^ "_bn"), []), q_bn) lthy16;
   val inj_unfolded = map (Local_Defs.unfold lthy17 @{thms alpha_gen}) alpha_inj
-  val q_inj_pre = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy17, th))) inj_unfolded;
+  val q_inj_pre = map (lift_thm lthy17) inj_unfolded;
   val q_inj = map (Local_Defs.fold lthy17 @{thms alpha_gen}) q_inj_pre
   val (_, lthy18) = Local_Theory.note ((Binding.name (q_name ^ "_inject"), []), q_inj) lthy17;
   val rel_dists = flat (map (distinct_rel lthy18 alpha_cases)
     (rel_distinct ~~ (List.take (alpha_ts, (length dts)))))
-  val q_dis = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy18, th))) rel_dists;
+  val q_dis = map (lift_thm lthy18) rel_dists;
   val (_, lthy19) = Local_Theory.note ((Binding.name (q_name ^ "_distinct"), []), q_dis) lthy18;
-  val q_eqvt = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy19, th))) raw_fv_bv_eqvt;
+  val q_eqvt = map (lift_thm lthy19) raw_fv_bv_eqvt;
   val (_, lthy20) = Local_Theory.note ((Binding.empty,
     [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19;
 in
@@ -405,6 +411,7 @@
 end
 *}
 
+
 ML {* 
 (* parsing the datatypes and declaring *)
 (* constructors in the local theory    *)