# HG changeset patch
# User blanchet
# Date 1409695578 -7200
# Node ID d91c1e50b36ed352404eda0d4750ed832e70374c
# Parent  3cfbb68ad2e07f6556b4def093570a6dd241e765
codatatypes are not datatypes

diff -r 3cfbb68ad2e0 -r d91c1e50b36e src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Wed Sep 03 00:06:17 2014 +0200
+++ b/src/HOL/Complex.thy	Wed Sep 03 00:06:18 2014 +0200
@@ -11,11 +11,9 @@
 begin
 
 text {*
-
-We use the @{text codatatype}-command to define the type of complex numbers. This might look strange
-at first, but allows us to use @{text primcorec} to define complex-functions by defining their
-real and imaginary result separate.
-
+We use the @{text codatatype} command to define the type of complex numbers. This allows us to use
+@{text primcorec} to define complex functions by defining their real and imaginary result
+separately.
 *}
 
 codatatype complex = Complex (Re: real) (Im: real)
diff -r 3cfbb68ad2e0 -r d91c1e50b36e src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Wed Sep 03 00:06:17 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Wed Sep 03 00:06:18 2014 +0200
@@ -265,8 +265,9 @@
 
 fun new_interpretation_of nesting_pref f (fp_sugars : fp_sugar list) thy =
   let val T_names = map (fst o dest_Type o #T) fp_sugars in
-    if nesting_pref = Keep_Nesting orelse
-        exists (is_none o Old_Datatype_Data.get_info thy) T_names then
+    if forall (curry (op =) Least_FP o #fp) fp_sugars andalso
+        (nesting_pref = Keep_Nesting orelse
+         exists (is_none o Old_Datatype_Data.get_info thy) T_names) then
       f Old_Datatype_Aux.default_config T_names thy
     else
       thy