changeset 58240 | b05ed697708e |
parent 58239 | 1c5bc387bd4c |
child 58446 | e89f57d1e46c |
--- 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*)