diff -r 59f59f826afd -r 2a75139b5931 src/HOL/Tools/BNF/bnf_gfp_grec.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Mon Oct 24 20:32:02 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Mon Oct 24 20:32:02 2016 +0200
@@ -3112,7 +3112,8 @@
     val _ = (case filter_out (member (op =) As o TFree) k_As of [] => ()
       | k_A :: _ => error ("Cannot have type variable " ^
           quote (Syntax.string_of_typ lthy (TFree k_A)) ^
-          " in the argument types when it does not occur in the result type"));
+          " in the argument types when it does not occur as an immediate argument of the result \
+          \type constructor"));
 
     val substDT = Term.typ_subst_atomic (Ds ~~ res_Ds);