added system option record_proofs, which allows to build HOL-Proofs without special Proofs.thy;

--- a/NEWS	Sun Apr 09 19:56:52 2017 +0200
+++ b/NEWS	Sun Apr 09 20:17:00 2017 +0200
@@ -166,6 +166,14 @@
 ISABELLE_PLATFORM64.
 
 
+*** System ***
+
+* System option "record_proofs" allows to change the global
+Proofterm.proofs variable for a session. Regular values are are 0, 1, 2;
+a negative value means the current state in the ML heap image remains
+unchanged.
+
+
 
 New in Isabelle2016-1 (December 2016)
 -------------------------------------

--- a/etc/options	Sun Apr 09 19:56:52 2017 +0200
+++ b/etc/options	Sun Apr 09 20:17:00 2017 +0200
@@ -82,6 +82,8 @@
 
 section "Detail of Proof Checking"
 
+option record_proofs : int = -1
+  -- "set level of proofterm recording: 0, 1, 2, negative means unchanged"
 option quick_and_dirty : bool = false
   -- "if true then some tools will OMIT some proofs"
 option skip_proofs : bool = false

--- a/src/HOL/Proofs.thy	Sun Apr 09 19:56:52 2017 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-theory Proofs
-imports Pure
-begin
-
-ML "Proofterm.proofs := 2"
-
-end
-

--- a/src/HOL/ROOT	Sun Apr 09 19:56:52 2017 +0200
+++ b/src/HOL/ROOT	Sun Apr 09 20:17:00 2017 +0200
@@ -18,8 +18,7 @@
   description {*
     HOL-Main with explicit proof terms.
   *}
-  options [document = false, quick_and_dirty = false, parallel_proofs = 0]
-  theories Proofs (*sequential change of global flag!*)
+  options [document = false, quick_and_dirty = false, record_proofs = 2, parallel_proofs = 0]
   theories "~~/src/HOL/Library/Old_Datatype"
   files
     "Tools/Quickcheck/Narrowing_Engine.hs"

--- a/src/Pure/System/isabelle_process.ML	Sun Apr 09 19:56:52 2017 +0200
+++ b/src/Pure/System/isabelle_process.ML	Sun Apr 09 20:17:00 2017 +0200
@@ -219,6 +219,8 @@
   Multithreading.trace := Options.default_int "threads_trace";
   Multithreading.max_threads_update (Options.default_int "threads");
   Goal.parallel_proofs := Options.default_int "parallel_proofs";
+  let val proofs = Options.default_int "record_proofs"
+  in if proofs < 0 then () else Proofterm.proofs := proofs end;
   Printer.show_markup_default := false);
 
 fun init_options_interactive () =