src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
changeset 58310 91ea607a34d8
parent 58290 14e186d2dd3a
child 58315 6d8458bc6e27
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Thu Sep 11 19:32:36 2014 +0200
@@ -341,7 +341,7 @@
     fun not_co_datatype (T as Type (s, _)) =
         if fp = Least_FP andalso
            is_some (Old_Datatype_Data.get_info (Proof_Context.theory_of lthy) s) then
-          error (qsoty T ^ " is not a new-style datatype (cf. \"datatype_new\")")
+          error (qsoty T ^ " is not a new-style datatype (cf. \"datatype\")")
         else
           not_co_datatype0 T
       | not_co_datatype T = not_co_datatype0 T;