src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML

     val i = length (binder_types (fastype_of f)) - length args
   in funpow i (fn th => th RS meta_fun_cong) th end;
 
 fun declare_names s xs ctxt =
   let
-    val res = Name.names ctxt s xs
+    val res = Name.invent_names ctxt s xs
   in (res, fold Name.declare (map fst res) ctxt) end
   
 fun split_all_pairs thy th =
   let
     val ctxt = Proof_Context.init_global thy