--- a/Nominal/Fv.thy	Thu Mar 18 08:03:42 2010 +0100
+++ b/Nominal/Fv.thy	Thu Mar 18 08:32:55 2010 +0100
@@ -754,16 +754,6 @@
       | 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
-*}
-
 lemma not_in_union: "c \<notin> a \<union> b \<equiv> (c \<notin> a \<and> c \<notin> b)"
 by auto