diff -r b39354db8629 -r 53b3c532a082 src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Sun Sep 23 14:52:53 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Sun Sep 23 14:52:53 2012 +0200
@@ -2396,7 +2396,7 @@
               |> Thm.close_derivation)
           end;
 
-        val map_unique_thm =
+        val dtor_map_unique_thm =
           let
             fun mk_prem u map dtor dtor' =
               mk_Trueprop_eq (HOLogic.mk_comp (dtor', u),
@@ -2408,7 +2408,7 @@
           in
             Skip_Proof.prove lthy [] []
               (fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal)))
-              (mk_map_unique_tac dtor_unfold_unique_thm map_comps)
+              (mk_dtor_map_unique_tac dtor_unfold_unique_thm map_comps)
               |> Thm.close_derivation
           end;
 
@@ -2933,7 +2933,7 @@
         val ls' = if m = 1 then [0] else ls;
 
         val Jbnf_common_notes =
-          [(map_uniqueN, [fold_maps map_unique_thm])] @
+          [(dtor_map_uniqueN, [fold_maps dtor_map_unique_thm])] @
           map2 (fn i => fn thm => (mk_dtor_set_inductN i, [thm])) ls' dtor_set_induct_thms
           |> map (fn (thmN, thms) =>
             ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));