author | panny |
Mon, 14 Jul 2014 01:22:59 +0200 | |
changeset 57549 | 7a2fbd8c1d98 |
parent 57548 | 278ab871319f |
child 57550 | 934a54d04a9a |
--- 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