# HG changeset patch
# User wenzelm
# Date 1415997410 -3600
# Node ID 272d7fb92396f84348e3ce2bbbca4bbf44827d10
# Parent  1c54ebc68394a9e1d525b44d7f999f50ec0b47b0
no quick_and_dirty for proof extraction, to avoid obscure errors like "corr: bad proof";

diff -r 1c54ebc68394 -r 272d7fb92396 src/HOL/ROOT
--- a/src/HOL/ROOT	Fri Nov 14 17:07:06 2014 +0100
+++ b/src/HOL/ROOT	Fri Nov 14 21:36:50 2014 +0100
@@ -19,7 +19,7 @@
   description {*
     HOL-Main with explicit proof terms.
   *}
-  options [document = false]
+  options [document = false, quick_and_dirty = false]
   theories Proofs (*sequential change of global flag!*)
   theories "~~/src/HOL/Library/Old_Datatype"
   files
@@ -400,7 +400,7 @@
   description {*
     Examples for program extraction in Higher-Order Logic.
   *}
-  options [condition = ML_SYSTEM_POLYML, parallel_proofs = 0]
+  options [condition = ML_SYSTEM_POLYML, parallel_proofs = 0, quick_and_dirty = false]
   theories [document = false]
     "~~/src/HOL/Library/Code_Target_Numeral"
     "~~/src/HOL/Library/Monad_Syntax"
@@ -425,7 +425,8 @@
     The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole
     theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html).
   *}
-  options [document_graph, print_mode = "no_brackets", parallel_proofs = 0]
+  options [document_graph, print_mode = "no_brackets", parallel_proofs = 0,
+    quick_and_dirty = false]
   theories [document = false]
     "~~/src/HOL/Library/Code_Target_Int"
   theories