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