--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Thu Jan 09 16:40:50 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Thu Jan 09 17:13:05 2014 +0100
@@ -719,7 +719,7 @@
dissect_coeqn_code lthy has_call fun_names basic_ctr_specss eqn_pos eqn0 concl matchedsss
|>> flat
else
- primcorec_error_eqn "malformed constructor or code view equation" eqn
+ primcorec_error_eqn "cannot mix constructor and code views (see manual for details)" eqn
else
primcorec_error_eqn "malformed function equation" eqn
end;