--- a/src/Doc/Datatypes/Datatypes.thy Tue Mar 04 08:19:04 2014 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy Tue Mar 04 10:35:37 2014 +0100
@@ -1713,8 +1713,8 @@
\begin{indentblock}
\begin{description}
-\item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.disc_corec} @{text t.disc_corec_iff}] ~ \\
-@{text t.sel_corec} @{text t.map} @{text t.rel_inject} @{text t.rel_distinct} @{text t.set}
+\item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.disc_corec_iff}] @{text t.sel_corec} ~ \\
+@{text t.map} @{text t.rel_inject} @{text t.rel_distinct} @{text t.set}
\end{description}
\end{indentblock}
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Tue Mar 04 08:19:04 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Tue Mar 04 10:35:37 2014 +0100
@@ -2376,7 +2376,6 @@
fun Jrel_coinduct_tac {context = ctxt, prems = CIHs} =
let
-val lthy = Config.put quick_and_dirty false lthy (*XXX*)
fun mk_helper_prem phi in_phi zip x y map map' dtor dtor' =
let
val zipxy = zip $ x $ y;