fix typo
authorpanny
Mon, 14 Jul 2014 01:59:23 +0200
changeset 57551 c07bac41c7ab
parent 57550 934a54d04a9a
child 57552 1072599c43f6
fix typo
src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Jul 14 01:35:43 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Jul 14 01:59:23 2014 +0200
@@ -938,7 +938,7 @@
           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,
-          code_rhs_opt = Option.map #ctr_rhs_opt sel_eqn_opt |> the_default NONE,
+          code_rhs_opt = Option.map #code_rhs_opt sel_eqn_opt |> the_default NONE,
           eqn_pos = Option.map (curry (op +) 1 o #eqn_pos) sel_eqn_opt |> the_default 100000 (* FIXME *),
           user_eqn = undef_const};
       in