--- 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)
--- 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