# HG changeset patch
# User blanchet
# Date 1410210544 -7200
# Node ID b05ed697708eda98c25bb5de5446270f3ce19c25
# Parent  1c5bc387bd4c791f7d9c6c28f28e58008a147c32
removed comment (yes, this is different -- add_typedef_global will fail in a locale with assumptions)

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