# HG changeset patch
# User blanchet
# Date 1377747718 -7200
# Node ID b40265203fb2ebdb9f86d359f94604e95e652d1e
# Parent  16235bb41881acea808e8234eff23daff634d4b7
more

diff -r 16235bb41881 -r b40265203fb2 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Aug 28 18:44:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Aug 29 05:41:58 2013 +0200
@@ -1138,8 +1138,8 @@
           in
             if is_some (bnf_of no_defs_lthy bad_tc) orelse
                is_some (fp_sugar_of no_defs_lthy bad_tc) then
-              error ("Non-strictly-positive " ^ co_prefix fp ^ "recursive occurrence of type " ^
-                fake_T ^ " in type expression " ^ fake_T_backdrop)
+              error ("Inadmissible " ^ co_prefix fp ^ "recursive occurrence of type " ^ fake_T ^
+                " in type expression " ^ fake_T_backdrop)
             else if is_some (Datatype_Data.get_info (Proof_Context.theory_of no_defs_lthy)
                 bad_tc) then
               error ("Unsupported " ^ co_prefix fp ^ "recursive occurrence of type " ^ fake_T ^