1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Tue Sep 24 18:07:09 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Tue Sep 24 19:15:49 2013 +0200
     1.3 @@ -195,7 +195,7 @@
     1.4      massage_call
     1.5    end;
     1.6  
     1.7 -fun massage_let_and_if ctxt has_call massage_leaf U =
     1.8 +fun massage_let_if ctxt has_call massage_leaf U =
     1.9    let
    1.10      val check_cond = ((not o has_call) orf unexpected_corec_call ctxt);
    1.11      fun massage_rec t =
    1.12 @@ -208,7 +208,7 @@
    1.13      massage_rec
    1.14    end;
    1.15  
    1.16 -fun fold_rev_let_and_if f =
    1.17 +fun fold_rev_let_if f =
    1.18    let
    1.19      fun fld t =
    1.20        (case Term.strip_comb t of
    1.21 @@ -220,7 +220,7 @@
    1.22    end;
    1.23  
    1.24  fun massage_direct_corec_call ctxt has_call raw_massage_call U t =
    1.25 -  massage_let_and_if ctxt has_call raw_massage_call U t;
    1.26 +  massage_let_if ctxt has_call raw_massage_call U t;
    1.27  
    1.28  fun massage_indirect_corec_call ctxt has_call raw_massage_call bound_Ts U t =
    1.29    let
    1.30 @@ -256,7 +256,7 @@
    1.31          handle AINT_NO_MAP _ => massage_direct_fun U T t;
    1.32  
    1.33      fun massage_call U T =
    1.34 -      massage_let_and_if ctxt has_call (fn t =>
    1.35 +      massage_let_if ctxt has_call (fn t =>
    1.36          if has_call t then
    1.37            (case U of
    1.38              Type (s, Us) =>
    1.39 @@ -304,15 +304,15 @@
    1.40  fun expand_corec_code_rhs ctxt has_call bound_Ts t =
    1.41    (case fastype_of1 (bound_Ts, t) of
    1.42      T as Type (s, Ts) =>
    1.43 -    massage_let_and_if ctxt has_call (fn t =>
    1.44 +    massage_let_if ctxt has_call (fn t =>
    1.45        if can (dest_ctr ctxt s) t then t
    1.46 -      else massage_let_and_if ctxt has_call I T (expand_ctr_term ctxt s Ts t)) T t
    1.47 +      else massage_let_if ctxt has_call I T (expand_ctr_term ctxt s Ts t)) T t
    1.48    | _ => raise Fail "expand_corec_code_rhs");
    1.49  
    1.50  fun massage_corec_code_rhs ctxt massage_ctr =
    1.51 -  massage_let_and_if ctxt (K false) (uncurry massage_ctr o Term.strip_comb);
    1.52 +  massage_let_if ctxt (K false) (uncurry massage_ctr o Term.strip_comb);
    1.53  
    1.54 -fun fold_rev_corec_code_rhs f = fold_rev_let_and_if (uncurry f o Term.strip_comb);
    1.55 +fun fold_rev_corec_code_rhs f = fold_rev_let_if (uncurry f o Term.strip_comb);
    1.56  
    1.57  fun add_conjuncts (Const (@{const_name conj}, _) $ t $ t') = add_conjuncts t o add_conjuncts t'
    1.58    | add_conjuncts t = cons t;