removed comment (yes, this is different -- add_typedef_global will fail in a locale with assumptions)
--- 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*)