# HG changeset patch
# User blanchet
# Date 1376335837 -7200
# Node ID 729ed0c46e180e2c491e53e7d93177fe1501a9f5
# Parent  d1bdc6a974605d4b22827e60cc104fc289bbdb67
qualify intermediate typedefs

diff -r d1bdc6a97460 -r 729ed0c46e18 src/HOL/BNF/Tools/bnf_gfp.ML
--- 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)
diff -r d1bdc6a97460 -r 729ed0c46e18 src/HOL/BNF/Tools/bnf_lfp.ML
--- 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)