changeset 49498 | acc583e14167 |
parent 49478 | 416ad6e2343b |
child 49499 | 464812bef4d9 |
--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Fri Sep 21 13:56:57 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Fri Sep 21 15:53:29 2012 +0200 @@ -64,7 +64,7 @@ val ks = 1 upto n; val m = live - n (*passive, if 0 don't generate a new BNF*); val ls = 1 upto m; - val b = Binding.name (mk_common_name bs); + val b = Binding.name (mk_common_name (map Binding.name_of bs)); (* TODO: check if m, n, etc., are sane *)