1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Apr 23 10:23:26 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Apr 23 10:23:26 2014 +0200
     1.3 @@ -239,7 +239,7 @@
     1.4      val co_recs = of_fp_res #xtor_co_recs;
     1.5      val ns = map (length o #Ts o #fp_res) fp_sugars;
     1.6  
     1.7 -    fun substT rho (Type (@{type_name "fun"}, [T, U])) = substT rho T --> substT rho U
     1.8 +    fun substT rho (Type (@{type_name fun}, [T, U])) = substT rho T --> substT rho U
     1.9        | substT rho (Type (s, Ts)) = Type (s, map (typ_subst_nonatomic rho) Ts)
    1.10        | substT _ T = T;
    1.11