diff -r d59f851926c5 -r 7e28654a760a Nominal/Fv.thy
--- a/Nominal/Fv.thy	Thu Mar 11 15:10:07 2010 +0100
+++ b/Nominal/Fv.thy	Thu Mar 11 16:12:15 2010 +0100
@@ -174,7 +174,7 @@
       in
         if arg_no mem args_in_bn then 
           (if is_rec_type dt then
-            (if body_index dt = ith_dtyp then fvbn $ x else error "fv_bn: not good")
+            (if body_index dt = ith_dtyp then fvbn $ x else error "fv_bn: recursive argument, but wrong datatype.")
           else @{term "{} :: atom set"}) else
         if is_atom thy ty then mk_single_atom x else
         if is_atom_set thy ty then mk_atoms x else
@@ -384,7 +384,7 @@
   val fv_names_all = fv_names_fst @ fv_bn_names;
   val add_binds = map (fn x => (Attrib.empty_binding, x))
 (* Function_Fun.add_fun Function_Common.default_config ... true *)
-  val _ = map tracing (map (Syntax.string_of_term @{context}) fv_eqs_all)
+(*  val _ = map tracing (map (Syntax.string_of_term @{context}) fv_eqs_all)*)
   val (fvs, lthy') = (Primrec.add_primrec
     (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_all) (add_binds fv_eqs_all) lthy)
   val (fvs2, lthy'') =
@@ -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