merge

--- a/src/Doc/Datatypes/Datatypes.thy	Fri Sep 13 14:57:20 2013 -0700
+++ b/src/Doc/Datatypes/Datatypes.thy	Tue Sep 17 01:11:37 2013 +0200
@@ -1602,7 +1602,7 @@
 
 \item The \emph{constructor view} specifies $f$ by equations of the form
 \[@{text "f x\<^sub>1 \<dots> x\<^sub>n = \<dots>"}\]
-Haskell and other lazy functional programming languages support this style.
+Lazy functional programming languages such as Haskell support this style.
 
 \item The \emph{destructor view} specifies $f$ by implications of the form
 \[@{text "\<dots> \<Longrightarrow> is_C\<^sub>j (f x\<^sub>1 \<dots> x\<^sub>n)"}\] and
@@ -1623,6 +1623,8 @@
     primcorec_notyet literate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where
       "literate f x = LCons x (literate f (f x))"
 
+text {* \blankline *}
+
     primcorec_notyet siterate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a stream" where
       "siterate f x = SCons x (siterate f (f x))"
 
@@ -1650,6 +1652,8 @@
       "ltl (literate f x) = literate f (f x)"
     .
 
+text {* \blankline *}
+
     primcorec siterate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a stream" where
       "shd (siterate _ x) = x" |
       "stl (siterate f x) = siterate f (f x)"
@@ -1851,6 +1855,8 @@
     primcorec_notyet iterate\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>i" where
       "iterate\<^sub>i\<^sub>i f x = Node\<^sub>i\<^sub>i x (lmap (iterate\<^sub>i\<^sub>i f) (f x))"
 
+text {* \blankline *}
+
     primcorec_notyet iterate\<^sub>i\<^sub>s :: "('a \<Rightarrow> 'a fset) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>s" where
       "iterate\<^sub>i\<^sub>s f x = Node\<^sub>i\<^sub>s x (fmap (iterate\<^sub>i\<^sub>s f) (f x))"
 

--- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Fri Sep 13 14:57:20 2013 -0700
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Tue Sep 17 01:11:37 2013 +0200
@@ -158,8 +158,8 @@
           derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
             dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs kss mss ns ctr_defss
             ctr_sugars co_iterss co_iter_defss (Proof_Context.export lthy no_defs_lthy) lthy
-          |> (fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _), _, _,
-                  (disc_unfold_thmss, disc_corec_thmss, _),
+          |> (fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _), _,
+                  (disc_unfold_thmss, disc_corec_thmss, _), _,
                   (sel_unfold_thmsss, sel_corec_thmsss, _)) =>
             (map snd coinduct_thms_pairs, unfold_thmss, corec_thmss, disc_unfold_thmss,
              disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss));