--- a/src/HOL/BNF/Tools/bnf_gfp.ML Mon Aug 12 21:30:36 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Mon Aug 12 21:30:37 2013 +0200
@@ -964,7 +964,8 @@
then (lthy, sum_bd, sum_bdT, bd_card_order, bd_Cinfinite, bd_Card_order, set_bdss)
else
let
- val sbdT_bind = Binding.suffix_name ("_" ^ sum_bdTN) b;
+ val sbdT_bind =
+ Binding.qualify false (Binding.name_of b) (Binding.suffix_name ("_" ^ sum_bdTN) b);
val ((sbdT_name, (sbdT_glob_info, sbdT_loc_info)), lthy) =
typedef (sbdT_bind, dead_params, NoSyn)