# HG changeset patch
# User blanchet
# Date 1382104927 -7200
# Node ID 5874be04e1f902ed7c176957ff0a5afcc03895a5
# Parent  a8cf84bfa9beab42d4de658f158297b78fad7191
tuning

diff -r a8cf84bfa9be -r 5874be04e1f9 src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Fri Oct 18 15:42:55 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Fri Oct 18 16:02:07 2013 +0200
@@ -172,26 +172,27 @@
   let
     fun subst bound_Ts (Abs (v, T, b)) = Abs (v, T, subst (T :: bound_Ts) b)
       | subst bound_Ts (t as g' $ y) =
-        let
-          val maybe_mutual_y' = AList.lookup (op =) mutual_calls y;
-          val maybe_nested_y' = AList.lookup (op =) nested_calls y;
-          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 not (member (op =) ctr_args y) then
-            pairself (subst bound_Ts) (g', y) |> (op $)
-          else if ctr_pos >= 0 then
-            list_comb (the maybe_mutual_y', g_args)
-          else if is_some maybe_nested_y' 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 (the maybe_nested_y')
-            |> (if has_call g' then I else curry (op $) g')
-          else
-            t
-        end
+        if not (member (op =) ctr_args y) then
+          pairself (subst bound_Ts) (g', y) |> op $
+        else
+          let
+            val maybe_mutual_y' = AList.lookup (op =) mutual_calls y;
+            val maybe_nested_y' = AList.lookup (op =) nested_calls y;
+            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 ctr_pos >= 0 then
+              list_comb (the maybe_mutual_y', g_args)
+            else if is_some maybe_nested_y' 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 (the maybe_nested_y')
+              |> (if has_call g' then I else curry (op $) g')
+            else
+              t
+          end
       | subst _ t = t
   in
     subst [] t