qualify intermediate typedefs

--- 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)

--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Mon Aug 12 21:30:36 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Mon Aug 12 21:30:37 2013 +0200
@@ -786,7 +786,7 @@
     val timer = time (timer "Minimal algebra definition & thms");
 
     val II_repT = HOLogic.mk_prodT (HOLogic.mk_tupleT II_BTs, HOLogic.mk_tupleT II_sTs);
-    val IIT_bind = Binding.suffix_name ("_" ^ IITN) b;
+    val IIT_bind = Binding.qualify false (Binding.name_of b) (Binding.suffix_name ("_" ^ IITN) b);
 
     val ((IIT_name, (IIT_glob_info, IIT_loc_info)), lthy) =
       typedef (IIT_bind, params, NoSyn)