# HG changeset patch
# User panny
# Date 1381526130 -7200
# Node ID 0b58c15ad284aaca26f1f92bc9bafa91e6673923
# Parent  07a8145aaebaacd01ab92f1ea11b26d030ef88a8
compile -- fix typo introduced in 07a8145aaeba

diff -r 07a8145aaeba -r 0b58c15ad284 src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Fri Oct 11 20:47:37 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Fri Oct 11 23:15:30 2013 +0200
@@ -976,11 +976,8 @@
                 fun prove_code_ctr {ctr, sels, ...} =
                   if not (exists (equal ctr o fst) ctr_alist) then NONE else
                     let
-                      val prems =
-                        (find_first (equal ctr o #ctr) disc_eqns,
-                         find_first (equal ctr o #ctr) sel_eqns)
-                        |>> Option.map #prems ||> Option.map #prems
-                        |> the o merge_options;
+                      val prems = find_first (equal ctr o #ctr) disc_eqns
+                        |> Option.map #prems |> the_default [];
                       val t =
                         filter (equal ctr o #ctr) sel_eqns
                         |> fst o finds ((op =) o apsnd #sel) sels