src/Pure/thm.ML
changeset 20071 8f3e1ddb50e6
parent 20057 058e913bac71
child 20261 af51389aa756
--- a/src/Pure/thm.ML	Tue Jul 11 12:16:52 2006 +0200
+++ b/src/Pure/thm.ML	Tue Jul 11 12:16:54 2006 +0200
@@ -1343,7 +1343,7 @@
     val short = length iparams - length cs;
     val newnames =
       if short < 0 then error "More names than abstractions!"
-      else variantlist (Library.take (short, iparams), cs) @ cs;
+      else Name.variant_list cs (Library.take (short, iparams)) @ cs;
     val freenames = map (#1 o dest_Free) (term_frees Bi);
     val newBi = Logic.list_rename_params (newnames, Bi);
   in