avoid infinite loop for unapplied terms + tuning

--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Thu Sep 19 11:27:32 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Thu Sep 19 12:20:12 2013 +0200
@@ -583,25 +583,23 @@
 fun build_corec_arg_indirect_call lthy has_call sel_eqns sel =
   let
     val maybe_sel_eqn = find_first (equal sel o #sel) sel_eqns;
-    fun rewrite _ _ =
-      let
-        fun subst (Abs (v, T, b)) = Abs (v, T, subst b)
-          | subst t =
-            let val (u, vs) = strip_comb t in
-              if is_Free u andalso has_call u then
-                Const (@{const_name Inr}, dummyT) $
-                  (if null vs then HOLogic.unit
-                   else foldr1 (fn (x, y) => Const (@{const_name Pair}, dummyT) $ x $ y) vs)
-              else if try (fst o dest_Const) u = SOME @{const_name prod_case} then
-                list_comb (u |> map_types (K dummyT), map subst vs)
-              else
-                list_comb (subst u, map subst vs)
-            end;
-      in
-        subst
-      end;
-    fun massage rhs_term t = massage_indirect_corec_call
-      lthy has_call rewrite [] (range_type (fastype_of t)) rhs_term;
+    fun rewrite (Abs (v, T, b)) = Abs (v, T, rewrite b)
+      | rewrite t =
+        let val (u, vs) = strip_comb t in
+          if is_Free u andalso has_call u then
+            Const (@{const_name Inr}, dummyT) $
+              (if null vs then HOLogic.unit
+               else foldr1 (fn (x, y) => Const (@{const_name Pair}, dummyT) $ x $ y) vs)
+          else if try (fst o dest_Const) u = SOME @{const_name prod_case} then
+            list_comb (u |> map_types (K dummyT), map rewrite vs)
+          else if null vs then
+            u
+          else
+            list_comb (rewrite u, map rewrite vs)
+        end;
+    fun massage rhs_term t =
+      massage_indirect_corec_call lthy has_call (K (K rewrite)) [] (range_type (fastype_of t))
+        rhs_term;
   in
     if is_none maybe_sel_eqn then I else
       abs_tuple (#fun_args (the maybe_sel_eqn)) o massage (#rhs_term (the maybe_sel_eqn))

--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Sep 19 11:27:32 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Sep 19 12:20:12 2013 +0200
@@ -150,7 +150,7 @@
     permute_like (op aconv) flat_fs fs flat_fs'
   end;
 
-fun massage_indirect_rec_call ctxt has_call massage_unapplied_direct_call bound_Ts y y' =
+fun massage_indirect_rec_call ctxt has_call raw_massage_fun bound_Ts y y' =
   let
     val typof = curry fastype_of1 bound_Ts;
     val build_map_fst = build_map ctxt (fst_const o fst);
@@ -161,11 +161,9 @@
     fun y_of_y' () = build_map_fst (yU, yT) $ y';
     val elim_y = Term.map_aterms (fn t => if t = y then y_of_y' () else t);
 
-    fun check_and_massage_unapplied_direct_call U T t =
-      if has_call t then
-        factor_out_types ctxt massage_unapplied_direct_call HOLogic.dest_prodT U T t
-      else
-        HOLogic.mk_comp (t, build_map_fst (U, T));
+    fun massage_direct_fun U T t =
+      if has_call t then factor_out_types ctxt raw_massage_fun HOLogic.dest_prodT U T t
+      else HOLogic.mk_comp (t, build_map_fst (U, T));
 
     fun massage_map (Type (_, Us)) (Type (s, Ts)) t =
         (case try (dest_map ctxt s) t of
@@ -184,7 +182,7 @@
         if has_call t then unexpected_rec_call ctxt t else t
       else
         massage_map U T t
-        handle AINT_NO_MAP _ => check_and_massage_unapplied_direct_call U T t;
+        handle AINT_NO_MAP _ => massage_direct_fun U T t;
 
     fun massage_call (t as t1 $ t2) =
         if t2 = y then
@@ -221,21 +219,21 @@
     fld
   end;
 
-fun massage_direct_corec_call ctxt has_call massage_direct_call U t =
-  massage_let_and_if ctxt has_call massage_direct_call U t;
+fun massage_direct_corec_call ctxt has_call raw_massage_call U t =
+  massage_let_and_if ctxt has_call raw_massage_call U t;
 
-fun massage_indirect_corec_call ctxt has_call massage_direct_call bound_Ts U t =
+fun massage_indirect_corec_call ctxt has_call raw_massage_call bound_Ts U t =
   let
     val typof = curry fastype_of1 bound_Ts;
     val build_map_Inl = build_map ctxt (uncurry Inl_const o dest_sumT o snd)
 
-    fun check_and_massage_direct_call U T t =
-      if has_call t then factor_out_types ctxt massage_direct_call dest_sumT U T t
+    fun massage_direct_call U T t =
+      if has_call t then factor_out_types ctxt raw_massage_call dest_sumT U T t
       else build_map_Inl (T, U) $ t;
 
-    fun check_and_massage_unapplied_direct_call U T t =
+    fun massage_direct_fun U T t =
       let val var = Var ((Name.uu, Term.maxidx_of_term t + 1), domain_type (typof t)) in
-        Term.lambda var (check_and_massage_direct_call U T (t $ var))
+        Term.lambda var (massage_direct_call U T (t $ var))
       end;
 
     fun massage_map (Type (_, Us)) (Type (s, Ts)) t =
@@ -255,7 +253,7 @@
         if has_call t then unexpected_corec_call ctxt t else t
       else
         massage_map U T t
-        handle AINT_NO_MAP _ => check_and_massage_unapplied_direct_call U T t;
+        handle AINT_NO_MAP _ => massage_direct_fun U T t;
 
     fun massage_call U T =
       massage_let_and_if ctxt has_call (fn t =>
@@ -271,12 +269,12 @@
               (case t of
                 t1 $ t2 =>
                 (if has_call t2 then
-                  check_and_massage_direct_call U T t
+                  massage_direct_call U T t
                 else
                   massage_map U T t1 $ t2
-                  handle AINT_NO_MAP _ => check_and_massage_direct_call U T t)
+                  handle AINT_NO_MAP _ => massage_direct_call U T t)
               | Abs (s, T', t') => Abs (s, T', massage_call (range_type U) (range_type T) t')
-              | _ => check_and_massage_direct_call U T t))
+              | _ => massage_direct_call U T t))
           | _ => ill_formed_corec_call ctxt t)
         else
           build_map_Inl (T, U) $ t) U