src/HOL/Tools/function_package/fundef_lib.ML

--- a/src/HOL/Tools/function_package/fundef_lib.ML	Wed Jul 19 11:55:26 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_lib.ML	Wed Jul 19 12:11:56 2006 +0200
@@ -48,7 +48,7 @@
 
 fun dest_all_all_ctx ctx (Const ("all", _) $ Abs (a as (n,T,b))) =
     let
-      val [(n', _)] = Variable.rename_wrt ctx [] [(n,T)]
+      val [(n', _)] = Variable.variant_frees ctx [] [(n,T)]
       val (_, ctx') = ProofContext.add_fixes_i [(n', SOME T, NoSyn)] ctx
 
       val (n'', body) = Term.dest_abs (n', T, b)