1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sun Sep 09 19:57:20 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sun Sep 09 21:13:15 2012 +0200
     1.3 @@ -166,8 +166,7 @@
     1.4        in snd oo add end;
     1.5  
     1.6      val nested_bnfs =
     1.7 -      map_filter (bnf_of lthy o Long_Name.base_name)
     1.8 -        (fold (fold (fold add_nested_bnf_names)) ctr_TsssXs []);
     1.9 +      map_filter (bnf_of lthy) (fold (fold (fold add_nested_bnf_names)) ctr_TsssXs []);
    1.10  
    1.11      val timer = time (Timer.startRealTimer ());
    1.12  
    1.13 @@ -456,7 +455,7 @@
    1.14  
    1.15      fun build_map build_arg (Type (s, Ts)) (Type (_, Us)) =
    1.16        let
    1.17 -        val map0 = map_of_bnf (the (bnf_of lthy (Long_Name.base_name s)));
    1.18 +        val map0 = map_of_bnf (the (bnf_of lthy s));
    1.19          val mapx = mk_map Ts Us map0;
    1.20          val TUs = map dest_funT (fst (split_last (fst (strip_map_type (fastype_of mapx)))));
    1.21          val args = map build_arg TUs;