--- 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);