# HG changeset patch
# User blanchet
# Date 1382102739 -7200
# Node ID b964fad0cbbd55d104f43a40dec7c7b3df6b9e49
# Parent  3fc041880014eaef7339583e001c314783f2c0d0
conceal more ugly constructions

diff -r 3fc041880014 -r b964fad0cbbd src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Fri Oct 18 15:19:21 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Fri Oct 18 15:25:39 2013 +0200
@@ -283,8 +283,8 @@
     (recs, ctr_poss)
     |-> map2 (fn recx => fn ctr_pos => list_comb (recx, rec_args) |> permute_args ctr_pos)
     |> Syntax.check_terms lthy
-    |> map3 (fn b => fn mx => fn t =>
-      ((b, mx), ((Binding.conceal (Binding.map_name Thm.def_name b), []), t))) bs mxs
+    |> map3 (fn b => fn mx => fn t => ((b, mx), ((Binding.conceal (Thm.def_binding b), []), t)))
+      bs mxs
   end;
 
 fun find_rec_calls has_call (eqn_data : eqn_data) =
@@ -778,8 +778,8 @@
     |> map2 (fn Ts => fn t => if length Ts = 0 then t $ HOLogic.unit else t) arg_Tss
     |> map2 currys arg_Tss
     |> Syntax.check_terms lthy
-    |> map3 (fn b => fn mx => fn t =>
-      ((b, mx), ((Binding.conceal (Binding.map_name Thm.def_name b), []), t))) bs mxs
+    |> map3 (fn b => fn mx => fn t => ((b, mx), ((Binding.conceal (Thm.def_binding b), []), t)))
+      bs mxs
     |> rpair exclss'
   end;
 
diff -r 3fc041880014 -r b964fad0cbbd src/HOL/BNF/Tools/ctr_sugar.ML
--- a/src/HOL/BNF/Tools/ctr_sugar.ML	Fri Oct 18 15:19:21 2013 +0200
+++ b/src/HOL/BNF/Tools/ctr_sugar.ML	Fri Oct 18 15:25:39 2013 +0200
@@ -392,7 +392,8 @@
          Term.lambda w (Library.foldr1 HOLogic.mk_disj (map3 mk_case_disj xctrs xfs xss)));
 
     val ((raw_case, (_, raw_case_def)), (lthy', lthy)) = no_defs_lthy
-      |> Local_Theory.define ((case_binding, NoSyn), ((Thm.def_binding case_binding, []), case_rhs))
+      |> Local_Theory.define ((case_binding, NoSyn),
+        ((Binding.conceal (Thm.def_binding case_binding), []), case_rhs))
       ||> `Local_Theory.restore;
 
     val phi = Proof_Context.export_morphism lthy lthy';