catch "not found" case
authorpanny
Mon, 14 Jul 2014 01:22:59 +0200
changeset 57549 7a2fbd8c1d98
parent 57548 278ab871319f
child 57550 934a54d04a9a
catch "not found" case
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