# HG changeset patch
# User panny
# Date 1405293779 -7200
# Node ID 7a2fbd8c1d98d73f64c2bda6f727e518cfe913b1
# Parent  278ab871319f4642863729f4da6dd4fd09bafefe
catch "not found" case

diff -r 278ab871319f -r 7a2fbd8c1d98 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Sat Jul 12 19:54:04 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Jul 14 01:22:59 2014 +0200
@@ -284,7 +284,8 @@
             | NONE =>
               let val (g, g_args) = strip_comb g' in
                 (case try (get_ctr_pos o fst o dest_Free) g of
-                  SOME ctr_pos =>
+                  SOME ~1 => subst_rec ()
+                | SOME ctr_pos =>
                   (length g_args >= ctr_pos orelse
                    raise PRIMREC ("too few arguments in recursive call", [t]);
                    (case AList.lookup (op =) mutual_calls y of