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