--- 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