discontinued system option "proofs" -- global state of Proofterm.proofs is persistently compiled into HOL-Proofs image;
discontinued unused proofterms for FOL;

--- a/NEWS	Sun Jun 30 11:37:34 2013 +0200
+++ b/NEWS	Sun Jun 30 12:30:02 2013 +0200
@@ -50,6 +50,11 @@
 
 *** Pure ***
 
+* System option "proofs" has been discontinued.  Instead the global
+state of Proofterm.proofs is persistently compiled into logic images
+as required, notably HOL-Proofs.  Users no longer need to change
+Proofterm.proofs dynamically.  Minor INCOMPATIBILITY.
+
 * Syntax translation functions (print_translation etc.) always depend
 on Proof.context.  Discontinued former "(advanced)" option -- this is
 now the default.  Minor INCOMPATIBILITY.

--- a/etc/options	Sun Jun 30 11:37:34 2013 +0200
+++ b/etc/options	Sun Jun 30 12:30:02 2013 +0200
@@ -79,8 +79,6 @@
 
 section "Detail of Proof Recording"
 
-option proofs : int = 1
-  -- "level of detail for proof objects: 0, 1, 2"
 option quick_and_dirty : bool = false
   -- "if true then some tools will OMIT some proofs"
 option skip_proofs : bool = false

--- a/src/Doc/ROOT	Sun Jun 30 11:37:34 2013 +0200
+++ b/src/Doc/ROOT	Sun Jun 30 12:30:02 2013 +0200
@@ -81,7 +81,7 @@
     Proof
     Syntax
     Tactic
-  theories [proofs = 2, skip_proofs = false, parallel_proofs = 0]
+  theories [skip_proofs = false, parallel_proofs = 0]
     Logic
   files
     "../prepare_document"

--- a/src/FOL/ROOT	Sun Jun 30 11:37:34 2013 +0200
+++ b/src/FOL/ROOT	Sun Jun 30 12:30:02 2013 +0200
@@ -15,7 +15,6 @@
 
     Michael Dummett, Elements of Intuitionism (Oxford, 1977)
   *}
-  options [proofs = 2]
   theories FOL
   files "document/root.tex"
 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Proofs.thy	Sun Jun 30 12:30:02 2013 +0200
@@ -0,0 +1,8 @@
+theory Proofs
+imports Pure
+begin
+
+ML "Proofterm.proofs := 2"
+
+end
+

--- a/src/HOL/ROOT	Sun Jun 30 11:37:34 2013 +0200
+++ b/src/HOL/ROOT	Sun Jun 30 12:30:02 2013 +0200
@@ -16,7 +16,8 @@
   description {*
     HOL-Main with explicit proof terms.
   *}
-  options [document = false, proofs = 2, skip_proofs = false]
+  options [document = false, skip_proofs = false]
+  theories Proofs (*sequential change of global flag!*)
   theories Main
   files
     "Tools/Quickcheck/Narrowing_Engine.hs"
@@ -356,7 +357,7 @@
   theories Decision_Procs
 
 session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
-  options [document = false, proofs = 2, skip_proofs = false, parallel_proofs = 0]
+  options [document = false, skip_proofs = false, parallel_proofs = 0]
   theories
     Hilbert_Classical
     XML_Data
@@ -365,7 +366,7 @@
   description {*
     Examples for program extraction in Higher-Order Logic.
   *}
-  options [condition = ISABELLE_POLYML, proofs = 2, skip_proofs = false, parallel_proofs = 0]
+  options [condition = ISABELLE_POLYML, skip_proofs = false, parallel_proofs = 0]
   theories [document = false]
     "~~/src/HOL/Library/Code_Target_Numeral"
     "~~/src/HOL/Library/Monad_Syntax"
@@ -390,8 +391,7 @@
     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", proofs = 2, skip_proofs = false,
-    parallel_proofs = 0]
+  options [document_graph, print_mode = "no_brackets", skip_proofs = false, parallel_proofs = 0]
   theories [document = false]
     "~~/src/HOL/Library/Code_Target_Int"
   theories
@@ -652,7 +652,7 @@
     MaSh_Export
     TPTP_Interpret
     THF_Arith
-  theories [proofs = 0]  (* FIXME !? *)
+  theories
     ATP_Problem_Import
 
 session "HOL-Multivariate_Analysis" (main) in Multivariate_Analysis = HOL +

--- a/src/Pure/Tools/build.ML	Sun Jun 30 11:37:34 2013 +0200
+++ b/src/Pure/Tools/build.ML	Sun Jun 30 12:30:02 2013 +0200
@@ -102,7 +102,6 @@
 
 fun use_theories last_timing options =
   Thy_Info.use_theories {last_timing = last_timing, master_dir = Path.current}
-    |> Unsynchronized.setmp Proofterm.proofs (Options.int options "proofs")
     |> Unsynchronized.setmp print_mode
         (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
     |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")