# HG changeset patch
# User blanchet
# Date 1437064576 -7200
# Node ID 6349a28af772ad33643c1dd54a79a05f57d5ef3a
# Parent  c0f6d90d0ae49161d39f7b69d48853f5c89f182f
made code less loopy

diff -r c0f6d90d0ae4 -r 6349a28af772 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Thu Jul 16 17:47:49 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Thu Jul 16 18:36:16 2015 +0200
@@ -366,18 +366,20 @@
         massage_map bound_Ts U T t
         handle NO_MAP _ => massage_mutual_fun bound_Ts U T t
     and massage_mutual_fun bound_Ts U T t =
-      (case t of
-        Const (@{const_name comp}, _) $ t1 $ t2 =>
-        if has_call t2 then massage_mutual_fun bound_Ts U T t
-        else mk_comp bound_Ts (massage_mutual_fun bound_Ts U T t1, t2)
-      | _ =>
-        let
-          val j = Term.maxidx_of_term t + 1;
-          val var = Var ((Name.uu, j), domain_type (fastype_of1 (bound_Ts, t)));
-        in
+      let
+        val j = Term.maxidx_of_term t + 1;
+        val var = Var ((Name.uu, j), domain_type (fastype_of1 (bound_Ts, t)));
+
+        fun massage_body () =
           Term.lambda var (Term.incr_boundvars 1 (massage_any_call bound_Ts U T
-            (betapply (t, var))))
-        end)
+            (betapply (t, var))));
+      in
+        (case t of
+          Const (@{const_name comp}, _) $ t1 $ t2 =>
+          if has_call t2 then massage_body ()
+          else mk_comp bound_Ts (massage_mutual_fun bound_Ts U T t1, t2)
+        | _ => massage_body ())
+      end
     and massage_any_call bound_Ts U T =
       massage_let_if_case_corec ctxt has_call (fn bound_Ts => fn t =>
         if has_call t then