# HG changeset patch
# User traytel
# Date 1418303658 -3600
# Node ID f2819313e3cc35e39cd04eb0077cec68f091aa1b
# Parent  894d613f7f7cb5db3ee885ce47fa054ef19f77e8
conceal typedef more violently

diff -r 894d613f7f7c -r f2819313e3cc src/HOL/Tools/BNF/bnf_util.ML
--- a/src/HOL/Tools/BNF/bnf_util.ML	Thu Dec 11 14:01:40 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Thu Dec 11 14:14:18 2014 +0100
@@ -147,7 +147,9 @@
     val b' = fold_rev Binding.prefix_name (map (suffix "_" o fst) (#2 (Binding.dest b))) b;
     val ((name, info), (lthy, lthy_old)) =
       lthy
+      |> Local_Theory.conceal
       |> Typedef.add_typedef true (b', Ts, mx) set opt_morphs tac
+      ||> Local_Theory.restore_naming lthy
       ||> `Local_Theory.restore;
     val phi = Proof_Context.export_morphism lthy_old lthy;
   in