diff -r 1c5bc387bd4c -r b05ed697708e src/HOL/Tools/BNF/bnf_util.ML
--- a/src/HOL/Tools/BNF/bnf_util.ML	Mon Sep 08 23:04:18 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Mon Sep 08 23:09:04 2014 +0200
@@ -317,7 +317,6 @@
 
 fun map_local_theory f = Named_Target.theory_init #> f #> Local_Theory.exit_global;
 
-(*TODO: is this really different from Typedef.add_typedef_global?*)
 fun typedef (b, Ts, mx) set opt_morphs tac lthy =
   let
     (*Work around loss of qualification in "typedef" axioms by replicating it in the name*)