Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
changeset 57549 7a2fbd8c1d98
parent 57527 1b07ca054327
child 57633 4ff8c090d580 
--- 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
isabelle