tuning

--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Tue Sep 24 18:07:09 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Tue Sep 24 19:15:49 2013 +0200
@@ -195,7 +195,7 @@
     massage_call
   end;
 
-fun massage_let_and_if ctxt has_call massage_leaf U =
+fun massage_let_if ctxt has_call massage_leaf U =
   let
     val check_cond = ((not o has_call) orf unexpected_corec_call ctxt);
     fun massage_rec t =
@@ -208,7 +208,7 @@
     massage_rec
   end;
 
-fun fold_rev_let_and_if f =
+fun fold_rev_let_if f =
   let
     fun fld t =
       (case Term.strip_comb t of
@@ -220,7 +220,7 @@
   end;
 
 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;
+  massage_let_if ctxt has_call raw_massage_call U t;
 
 fun massage_indirect_corec_call ctxt has_call raw_massage_call bound_Ts U t =
   let
@@ -256,7 +256,7 @@
         handle AINT_NO_MAP _ => massage_direct_fun U T t;
 
     fun massage_call U T =
-      massage_let_and_if ctxt has_call (fn t =>
+      massage_let_if ctxt has_call (fn t =>
         if has_call t then
           (case U of
             Type (s, Us) =>
@@ -304,15 +304,15 @@
 fun expand_corec_code_rhs ctxt has_call bound_Ts t =
   (case fastype_of1 (bound_Ts, t) of
     T as Type (s, Ts) =>
-    massage_let_and_if ctxt has_call (fn t =>
+    massage_let_if ctxt has_call (fn t =>
       if can (dest_ctr ctxt s) t then t
-      else massage_let_and_if ctxt has_call I T (expand_ctr_term ctxt s Ts t)) T t
+      else massage_let_if ctxt has_call I T (expand_ctr_term ctxt s Ts t)) T t
   | _ => raise Fail "expand_corec_code_rhs");
 
 fun massage_corec_code_rhs ctxt massage_ctr =
-  massage_let_and_if ctxt (K false) (uncurry massage_ctr o Term.strip_comb);
+  massage_let_if ctxt (K false) (uncurry massage_ctr o Term.strip_comb);
 
-fun fold_rev_corec_code_rhs f = fold_rev_let_and_if (uncurry f o Term.strip_comb);
+fun fold_rev_corec_code_rhs f = fold_rev_let_if (uncurry f o Term.strip_comb);
 
 fun add_conjuncts (Const (@{const_name conj}, _) $ t $ t') = add_conjuncts t o add_conjuncts t'
   | add_conjuncts t = cons t;