src/Pure/thm.ML
changeset 45328 e5b33eecbf6e
parent 44334 605381e7c7c5
child 45443 c8a9a5e577bd
--- a/src/Pure/thm.ML	Thu Nov 03 22:23:41 2011 +0100
+++ b/src/Pure/thm.ML	Thu Nov 03 22:51:37 2011 +0100
@@ -1494,7 +1494,7 @@
       if short < 0 then error "More names than abstractions!"
       else Name.variant_list cs (take short iparams) @ cs;
     val freenames = Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) Bi [];
-    val newBi = Logic.list_rename_params (newnames, Bi);
+    val newBi = Logic.list_rename_params newnames Bi;
   in
     (case duplicates (op =) cs of
       a :: _ => (warning ("Can't rename.  Bound variables not distinct: " ^ a); state)