# HG changeset patch
# User blanchet
# Date 1393925737 -3600
# Node ID 307115c3b9691c94bc96344e919a38ac7d4f0edd
# Parent  b9468e4e8c05e9828ae2389148afa5c7c25793a7# Parent  74a2758dcbae8d7f15e349eb9c9a8486feb3ea5b
merge

diff -r 74a2758dcbae -r 307115c3b969 src/Doc/Datatypes/Datatypes.thy
--- 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}
diff -r 74a2758dcbae -r 307115c3b969 src/HOL/Tools/BNF/bnf_gfp.ML
--- 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;