src/HOL/Codatatype/Tools/bnf_lfp.ML
changeset 49327 541d818d2ff3
parent 49313 3f8671b353ae
child 49330 276ff43ee0b1
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Wed Sep 12 10:36:00 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Wed Sep 12 11:38:22 2012 +0200
     1.3 @@ -33,7 +33,7 @@
     1.4      val n = length bnfs; (*active*)
     1.5      val ks = 1 upto n;
     1.6      val m = live - n; (*passive, if 0 don't generate a new bnf*)
     1.7 -    val b = Binding.name (fold_rev (fn b => fn s => Binding.name_of b ^ s) bs "");
     1.8 +    val b = Binding.name (mk_bundle_name bs);
     1.9  
    1.10      (* TODO: check if m, n etc are sane *)
    1.11