# HG changeset patch
# User blanchet
# Date 1379545765 -7200
# Node ID 73d63e2616aa8cce70224b72bc2cdc25d4037a4f
# Parent  e176d6d3345f69afb7b6292b8beb5b0abd845c35
generalize helper function

diff -r e176d6d3345f -r 73d63e2616aa src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Sep 19 00:32:33 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Sep 19 01:09:25 2013 +0200
@@ -193,22 +193,22 @@
     massage_call o Envir.beta_eta_contract
   end;
 
-fun massage_let_and_if ctxt has_call massage_rec massage_else U T t =
-  (case Term.strip_comb t of
-    (Const (@{const_name Let}, _), [arg1, arg2]) => massage_rec U T (betapply (arg2, arg1))
-  | (Const (@{const_name If}, _), arg :: args) =>
-    if has_call arg then unexpected_corec_call ctxt arg
-    else list_comb (If_const U $ arg, map (massage_rec U T) args)
-  | _ => massage_else U T t);
+fun massage_let_and_if ctxt check_cond massage_else =
+  let
+    fun massage_rec U T t =
+      (case Term.strip_comb t of
+        (Const (@{const_name Let}, _), [arg1, arg2]) => massage_rec U T (betapply (arg2, arg1))
+      | (Const (@{const_name If}, _), arg :: args) =>
+        list_comb (If_const U $ tap check_cond arg, map (massage_rec U T) args)
+      | _ => massage_else U T t)
+  in
+    massage_rec
+  end;
 
 fun massage_direct_corec_call ctxt has_call massage_direct_call bound_Ts res_U t =
-  let
-    val typof = curry fastype_of1 bound_Ts;
-
-    fun massage_call U T =
-      massage_let_and_if ctxt has_call massage_call massage_direct_call U T;
-  in
-    massage_call res_U (typof t) (Envir.beta_eta_contract t)
+  let val typof = curry fastype_of1 bound_Ts in
+    massage_let_and_if ctxt ((not o has_call) orf unexpected_corec_call ctxt) massage_direct_call
+      res_U (typof t) (Envir.beta_eta_contract t)
   end;
 
 fun massage_indirect_corec_call ctxt has_call massage_direct_call bound_Ts res_U t =
@@ -245,7 +245,7 @@
         handle AINT_NO_MAP _ => check_and_massage_unapplied_direct_call U T t;
 
     fun massage_call U T =
-      massage_let_and_if ctxt has_call massage_call
+      massage_let_and_if ctxt ((not o has_call) orf unexpected_corec_call ctxt)
         (fn U => fn T => fn t =>
             (case U of
               Type (s, Us) =>