Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
simplify code
authorblanchet
Sun, 20 Oct 2013 18:22:59 +0200
changeset 54165 6e01e29d34bc
parent 54164 800106c17419
child 54166 5086aac96846
simplify code
src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Sun Oct 20 17:45:54 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Sun Oct 20 18:22:59 2013 +0200
@@ -185,10 +185,8 @@
                 primrec_error_eqn "too few arguments in recursive call" t;
             in
               if is_some maybe_nested_y_head' then
-                (if has_call g' then t else y)
-                |> massage_nested_rec_call lthy has_call
-                  (rewrite_map_arg get_ctr_pos) bound_Ts y_head (the maybe_nested_y_head')
-                |> (if has_call g' then I else curry (op $) g')
+                massage_nested_rec_call lthy has_call
+                  (rewrite_map_arg get_ctr_pos) bound_Ts y_head (the maybe_nested_y_head') t
               else if ctr_pos >= 0 then
                 (case maybe_mutual_y' of
                   NONE => t
isabelle