# HG changeset patch
# User blanchet
# Date 1382289608 -7200
# Node ID ebdf8deafe1031f208ba96500c8b5f7c37234598
# Parent  5086aac9684694307d3ea10fcc5d77637e32ad50
tuning

diff -r 5086aac96846 -r ebdf8deafe10 src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Sun Oct 20 19:20:08 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Sun Oct 20 19:20:08 2013 +0200
@@ -176,22 +176,22 @@
             subst bound_Ts g' $ subst bound_Ts y
           else
             let
-              val maybe_mutual_y' = AList.lookup (op =) mutual_calls y;
-              val maybe_nested_y_head' = AList.lookup (op =) nested_calls y_head;
               val (g, g_args) = strip_comb g';
               val ctr_pos = try (get_ctr_pos o the) (free_name g) |> the_default ~1;
               val _ = ctr_pos < 0 orelse length g_args >= ctr_pos orelse
                 primrec_error_eqn "too few arguments in recursive call" t;
             in
-              if is_some maybe_nested_y_head' then
+              (case AList.lookup (op =) nested_calls y_head of
+                SOME y_head' =>
                 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
-                | SOME y' => list_comb (y', g_args))
-              else
-                t
+                  y_head' t
+              | NONE =>
+                if ctr_pos >= 0 then
+                  (case AList.lookup (op =) mutual_calls y of
+                    NONE => t
+                  | SOME y' => list_comb (y', g_args))
+                else
+                  t)
             end
         end
       | subst bound_Ts (Abs (v, T, b)) = Abs (v, T, subst (T :: bound_Ts) b)