1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Fri Oct 18 15:19:21 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Fri Oct 18 15:25:39 2013 +0200
     1.3 @@ -283,8 +283,8 @@
     1.4      (recs, ctr_poss)
     1.5      |-> map2 (fn recx => fn ctr_pos => list_comb (recx, rec_args) |> permute_args ctr_pos)
     1.6      |> Syntax.check_terms lthy
     1.7 -    |> map3 (fn b => fn mx => fn t =>
     1.8 -      ((b, mx), ((Binding.conceal (Binding.map_name Thm.def_name b), []), t))) bs mxs
     1.9 +    |> map3 (fn b => fn mx => fn t => ((b, mx), ((Binding.conceal (Thm.def_binding b), []), t)))
    1.10 +      bs mxs
    1.11    end;
    1.12  
    1.13  fun find_rec_calls has_call (eqn_data : eqn_data) =
    1.14 @@ -778,8 +778,8 @@
    1.15      |> map2 (fn Ts => fn t => if length Ts = 0 then t $ HOLogic.unit else t) arg_Tss
    1.16      |> map2 currys arg_Tss
    1.17      |> Syntax.check_terms lthy
    1.18 -    |> map3 (fn b => fn mx => fn t =>
    1.19 -      ((b, mx), ((Binding.conceal (Binding.map_name Thm.def_name b), []), t))) bs mxs
    1.20 +    |> map3 (fn b => fn mx => fn t => ((b, mx), ((Binding.conceal (Thm.def_binding b), []), t)))
    1.21 +      bs mxs
    1.22      |> rpair exclss'
    1.23    end;
    1.24  

     2.1 --- a/src/HOL/BNF/Tools/ctr_sugar.ML	Fri Oct 18 15:19:21 2013 +0200
     2.2 +++ b/src/HOL/BNF/Tools/ctr_sugar.ML	Fri Oct 18 15:25:39 2013 +0200
     2.3 @@ -392,7 +392,8 @@
     2.4           Term.lambda w (Library.foldr1 HOLogic.mk_disj (map3 mk_case_disj xctrs xfs xss)));
     2.5  
     2.6      val ((raw_case, (_, raw_case_def)), (lthy', lthy)) = no_defs_lthy
     2.7 -      |> Local_Theory.define ((case_binding, NoSyn), ((Thm.def_binding case_binding, []), case_rhs))
     2.8 +      |> Local_Theory.define ((case_binding, NoSyn),
     2.9 +        ((Binding.conceal (Thm.def_binding case_binding), []), case_rhs))
    2.10        ||> `Local_Theory.restore;
    2.11  
    2.12      val phi = Proof_Context.export_morphism lthy lthy';