diff -r 2c6851248b3f -r 542ff50555f5 Nominal/nominal_function_core.ML
--- a/Nominal/nominal_function_core.ML	Mon May 09 04:49:58 2011 +0100
+++ b/Nominal/nominal_function_core.ML	Tue May 10 07:47:06 2011 +0100
@@ -540,10 +540,10 @@
     fun requantify orig_intro thm =
       let
         val (qs, t) = dest_all_all orig_intro
-        val frees = frees_in_term lthy t |> remove (op =) (Binding.name_of R, T)
-        val vars = Term.add_vars (prop_of thm) [] |> rev
+        val frees = Variable.add_frees lthy t [] |> remove (op =) (Binding.name_of R, T)
+        val vars = Term.add_vars (prop_of thm) []
         val varmap = AList.lookup (op =) (frees ~~ map fst vars)
-          #> the_default ("",0)
+           #> the_default ("",0)
       in
         fold_rev (fn Free (n, T) =>
           forall_intr_rename (n, cert (Var (varmap (n, T), T)))) qs thm