diff -r 860b7c6bd913 -r acc583e14167 src/HOL/Codatatype/Tools/bnf_gfp.ML
--- 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 *)