# HG changeset patch # User panny # Date 1389291035 -3600 # Node ID 4933165fd1123a7789ca873694340306f385846e # Parent 99eebac5fcb3e68fe15bc17b2189262ad26e1b30 do not use wrong constructor in auto-generated proof goal diff -r 99eebac5fcb3 -r 4933165fd112 src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Thu Jan 09 17:51:52 2014 +0100 +++ b/src/Doc/Datatypes/Datatypes.thy Thu Jan 09 19:10:35 2014 +0100 @@ -201,6 +201,7 @@ (*<*) hide_const None Some + hide_type option (*>*) datatype_new 'a option = None | Some 'a diff -r 99eebac5fcb3 -r 4933165fd112 src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML --- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Thu Jan 09 17:51:52 2014 +0100 +++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Thu Jan 09 19:10:35 2014 +0100 @@ -850,17 +850,17 @@ let val n = 0 upto length ctr_specs |> the o find_first (fn idx => not (exists (curry (op =) idx o #ctr_no) disc_eqns)); + val {ctr, disc, ...} = nth ctr_specs n; val fun_args = (try (#fun_args o hd) disc_eqns, try (#fun_args o hd) sel_eqns) |> the_default (map (curry Free Name.uu) arg_Ts) o merge_options; - val sel_eqn_opt = - find_first (curry (op =) (Binding.name_of fun_binding) o #fun_name) sel_eqns; + val sel_eqn_opt = find_first (equal ctr o #ctr) sel_eqns; val extra_disc_eqn = { fun_name = Binding.name_of fun_binding, fun_T = arg_Ts ---> body_type (fastype_of (#ctr (hd ctr_specs))), fun_args = fun_args, - ctr = #ctr (nth ctr_specs n), + ctr = ctr, ctr_no = n, - disc = #disc (nth ctr_specs n), + disc = disc, prems = maps (s_not_conj o #prems) disc_eqns, auto_gen = true, ctr_rhs_opt = Option.map #ctr_rhs_opt sel_eqn_opt |> the_default NONE,