--- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML Sun Aug 14 12:26:09 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML Sun Aug 14 12:26:09 2016 +0200
@@ -3120,7 +3120,8 @@
val k_As = fold Term.add_tfreesT k_Ts0 [];
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)) ^ " used like that in friend"));
+ quote (Syntax.string_of_typ lthy (TFree k_A)) ^
+ " in the argument types when it does not occur in the result type"));
val substDT = Term.typ_subst_atomic (Ds ~~ res_Ds);