# HG changeset patch
# User blanchet
# Date 1471170369 -7200
# Node ID 94a89b95b871c88ff697537c7af1210335442aa2
# Parent  48a2c88091d7de9d3e985ab5990faf19b56086d5
tuned message

diff -r 48a2c88091d7 -r 94a89b95b871 src/HOL/Tools/BNF/bnf_gfp_grec.ML
--- 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);