src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
changeset 53736 82799e03fff7
parent 53735 99331dac1e1c
child 53743 87585d506db4
equal deleted inserted replaced
53735:99331dac1e1c 53736:82799e03fff7
   837             ((Binding.qualify true fun_name (@{binding sel}), simp_attrs), [(map snd thms, [])])));
   837             ((Binding.qualify true fun_name (@{binding sel}), simp_attrs), [(map snd thms, [])])));
   838         val ctr_notes =
   838         val ctr_notes =
   839           fun_names ~~ map5 (maps oooo prove_ctr) disc_thmss sel_thmss
   839           fun_names ~~ map5 (maps oooo prove_ctr) disc_thmss sel_thmss
   840             disc_eqnss sel_eqnss (map #ctr_specs corec_specs)
   840             disc_eqnss sel_eqnss (map #ctr_specs corec_specs)
   841           |> map (fn (fun_name, thms) =>
   841           |> map (fn (fun_name, thms) =>
   842             ((Binding.qualify true fun_name (@{binding ctr}), simp_attrs), [(thms, [])]));
   842             ((Binding.qualify true fun_name (@{binding ctr}), []), [(thms, [])]));
   843       in
   843       in
   844         lthy |> snd o Local_Theory.notes
   844         lthy |> snd o Local_Theory.notes
   845           (filter (not o null o fst o the_single o snd) (disc_notes @ sel_notes @ ctr_notes))
   845           (filter (not o null o fst o the_single o snd) (disc_notes @ sel_notes @ ctr_notes))
   846       end;
   846       end;
   847   in
   847   in