more uniform ML/document antiquotations;
authorwenzelm
Tue Apr 08 14:59:36 2014 +0200 (2014-04-08)
changeset 564678d7d6f17c6a7
parent 56466 08982abdcdad
child 56468 30128d1acfbc
more uniform ML/document antiquotations;
src/Doc/antiquote_setup.ML
src/HOL/Mutabelle/mutabelle_extra.ML
src/HOL/Prolog/prolog.ML
src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML
src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy
src/HOL/Tools/Nitpick/nitpick_commands.ML
src/HOL/Tools/SMT/smt_setup_solvers.ML
src/HOL/Tools/SMT2/smt2_systems.ML
src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
src/HOL/Tools/try0.ML
src/Pure/Isar/isar_syn.ML
src/Pure/ML/ml_antiquotations.ML
src/Pure/System/options.ML
src/Pure/Tools/find_theorems.ML
src/Pure/Tools/proof_general_pure.ML
src/Tools/quickcheck.ML
src/Tools/solve_direct.ML
src/Tools/try.ML
     1.1 --- a/src/Doc/antiquote_setup.ML	Tue Apr 08 14:56:55 2014 +0200
     1.2 +++ b/src/Doc/antiquote_setup.ML	Tue Apr 08 14:59:36 2014 +0200
     1.3 @@ -201,6 +201,10 @@
     1.4        val _ = Context_Position.reports ctxt (map (pair pos) markup);
     1.5      in true end;
     1.6  
     1.7 +fun check_system_option ctxt (name, pos) =
     1.8 +  (Context_Position.report ctxt pos (Options.default_markup (name, pos)); true)
     1.9 +    handle ERROR _ => false;
    1.10 +
    1.11  fun check_tool ctxt (name, pos) =
    1.12    let
    1.13      fun tool dir =
    1.14 @@ -265,7 +269,7 @@
    1.15      entity_antiqs (can o Thy_Output.check_command) "" @{binding antiquotation} #>
    1.16      entity_antiqs (can o Thy_Output.check_option) "" @{binding antiquotation_option} #>
    1.17      entity_antiqs no_check "isatt" @{binding setting} #>
    1.18 -    entity_antiqs no_check "isatt" @{binding system_option} #>
    1.19 +    entity_antiqs check_system_option "isatt" @{binding system_option} #>
    1.20      entity_antiqs no_check "" @{binding inference} #>
    1.21      entity_antiqs no_check "isatt" @{binding executable} #>
    1.22      entity_antiqs check_tool "isatool" @{binding tool} #>
     2.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Tue Apr 08 14:56:55 2014 +0200
     2.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Tue Apr 08 14:59:36 2014 +0200
     2.3 @@ -124,7 +124,7 @@
     2.4              | SOME _ => (GenuineCex, Quickcheck.timings_of result)
     2.5            end) ()
     2.6    handle TimeLimit.TimeOut =>
     2.7 -         (Timeout, [("timelimit", Real.floor (Options.default_real @{option auto_time_limit}))])
     2.8 +         (Timeout, [("timelimit", Real.floor (Options.default_real @{system_option auto_time_limit}))])
     2.9  
    2.10  fun quickcheck_mtd change_options quickcheck_generator =
    2.11    ("quickcheck_" ^ quickcheck_generator, invoke_quickcheck change_options)
     3.1 --- a/src/HOL/Prolog/prolog.ML	Tue Apr 08 14:56:55 2014 +0200
     3.2 +++ b/src/HOL/Prolog/prolog.ML	Tue Apr 08 14:59:36 2014 +0200
     3.3 @@ -2,7 +2,7 @@
     3.4      Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
     3.5  *)
     3.6  
     3.7 -Options.default_put_bool @{option show_main_goal} true;
     3.8 +Options.default_put_bool @{system_option show_main_goal} true;
     3.9  
    3.10  structure Prolog =
    3.11  struct
     4.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Tue Apr 08 14:56:55 2014 +0200
     4.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Tue Apr 08 14:59:36 2014 +0200
     4.3 @@ -285,7 +285,7 @@
     4.4  
     4.5  type tptp_problem = tptp_line list
     4.6  
     4.7 -fun debug f x = if Options.default_bool @{option ML_exception_trace} then (f x; ()) else ()
     4.8 +fun debug f x = if Options.default_bool @{system_option ML_exception_trace} then (f x; ()) else ()
     4.9  
    4.10  fun nameof_tff_atom_type (Atom_type str) = str
    4.11    | nameof_tff_atom_type _ = raise TPTP_SYNTAX "nameof_tff_atom_type called on non-atom type"
     5.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Tue Apr 08 14:56:55 2014 +0200
     5.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Tue Apr 08 14:59:36 2014 +0200
     5.3 @@ -42,7 +42,7 @@
     5.4  ML {*
     5.5    if test_all @{context} then ()
     5.6    else
     5.7 -    (Options.default_put_bool @{option ML_exception_trace} true;
     5.8 +    (Options.default_put_bool @{system_option ML_exception_trace} true;
     5.9       default_print_depth 200;  (* FIXME proper ML_print_depth within context!? *)
    5.10       PolyML.Compiler.maxInlineSize := 0)
    5.11  *}
     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_commands.ML	Tue Apr 08 14:56:55 2014 +0200
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML	Tue Apr 08 14:59:36 2014 +0200
     6.3 @@ -34,7 +34,7 @@
     6.4  val _ =
     6.5    ProofGeneral.preference_option ProofGeneral.category_tracing
     6.6      NONE
     6.7 -    @{option auto_nitpick}
     6.8 +    @{system_option auto_nitpick}
     6.9      "auto-nitpick"
    6.10      "Run Nitpick automatically"
    6.11  
    6.12 @@ -396,6 +396,6 @@
    6.13  
    6.14  fun try_nitpick auto = pick_nits [] (if auto then Auto_Try else Try) 1 0
    6.15  
    6.16 -val _ = Try.tool_setup (nitpickN, (50, @{option auto_nitpick}, try_nitpick))
    6.17 +val _ = Try.tool_setup (nitpickN, (50, @{system_option auto_nitpick}, try_nitpick))
    6.18  
    6.19  end;
     7.1 --- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Tue Apr 08 14:56:55 2014 +0200
     7.2 +++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Tue Apr 08 14:59:36 2014 +0200
     7.3 @@ -100,7 +100,7 @@
     7.4  
     7.5  fun z3_non_commercial () =
     7.6    let
     7.7 -    val flag1 = Options.default_string @{option z3_non_commercial}
     7.8 +    val flag1 = Options.default_string @{system_option z3_non_commercial}
     7.9      val flag2 = getenv "Z3_NON_COMMERCIAL"
    7.10    in
    7.11      if accepted flag1 then Z3_Non_Commercial_Accepted
     8.1 --- a/src/HOL/Tools/SMT2/smt2_systems.ML	Tue Apr 08 14:56:55 2014 +0200
     8.2 +++ b/src/HOL/Tools/SMT2/smt2_systems.ML	Tue Apr 08 14:59:36 2014 +0200
     8.3 @@ -97,7 +97,7 @@
     8.4  
     8.5  fun z3_non_commercial () =
     8.6    let
     8.7 -    val flag1 = Options.default_string @{option z3_non_commercial}
     8.8 +    val flag1 = Options.default_string @{system_option z3_non_commercial}
     8.9      val flag2 = getenv "Z3_NON_COMMERCIAL"
    8.10    in
    8.11      if accepted flag1 then Z3_Non_Commercial_Accepted
     9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Tue Apr 08 14:56:55 2014 +0200
     9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Tue Apr 08 14:59:36 2014 +0200
     9.3 @@ -43,7 +43,7 @@
     9.4  val _ =
     9.5    ProofGeneral.preference_option ProofGeneral.category_tracing
     9.6      NONE
     9.7 -    @{option auto_sledgehammer}
     9.8 +    @{system_option auto_sledgehammer}
     9.9      "auto-sledgehammer"
    9.10      "Run Sledgehammer automatically"
    9.11  
    9.12 @@ -72,7 +72,7 @@
    9.13  val _ =
    9.14    ProofGeneral.preference_option ProofGeneral.category_proof
    9.15      NONE
    9.16 -    @{option sledgehammer_timeout}
    9.17 +    @{system_option sledgehammer_timeout}
    9.18      "Sledgehammer: Time Limit"
    9.19      "ATPs will be interrupted after this time (in seconds)"
    9.20  
    9.21 @@ -229,7 +229,7 @@
    9.22      |> fold (AList.default (op =))
    9.23           [("provers", [(case !provers of "" => default_provers_param_value mode ctxt | s => s)]),
    9.24            ("timeout",
    9.25 -           let val timeout = Options.default_int @{option sledgehammer_timeout} in
    9.26 +           let val timeout = Options.default_int @{system_option sledgehammer_timeout} in
    9.27               [if timeout <= 0 then "none" else string_of_int timeout]
    9.28             end)]
    9.29    end
    9.30 @@ -472,7 +472,7 @@
    9.31        state
    9.32    end
    9.33  
    9.34 -val _ = Try.tool_setup (sledgehammerN, (40, @{option auto_sledgehammer}, try_sledgehammer))
    9.35 +val _ = Try.tool_setup (sledgehammerN, (40, @{system_option auto_sledgehammer}, try_sledgehammer))
    9.36  
    9.37  val _ =
    9.38    Query_Operation.register sledgehammerN (fn {state = st, args, output_result} =>
    10.1 --- a/src/HOL/Tools/try0.ML	Tue Apr 08 14:56:55 2014 +0200
    10.2 +++ b/src/HOL/Tools/try0.ML	Tue Apr 08 14:59:36 2014 +0200
    10.3 @@ -25,7 +25,7 @@
    10.4  val _ =
    10.5    ProofGeneral.preference_option ProofGeneral.category_tracing
    10.6      NONE
    10.7 -    @{option auto_methods}
    10.8 +    @{system_option auto_methods}
    10.9      "auto-try0"
   10.10      "Try standard proof methods";
   10.11  
   10.12 @@ -193,6 +193,6 @@
   10.13  
   10.14  fun try_try0 auto = generic_try0 (if auto then Auto_Try else Try) NONE ([], [], [], []);
   10.15  
   10.16 -val _ = Try.tool_setup (try0N, (30, @{option auto_methods}, try_try0));
   10.17 +val _ = Try.tool_setup (try0N, (30, @{system_option auto_methods}, try_try0));
   10.18  
   10.19  end;
    11.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Apr 08 14:56:55 2014 +0200
    11.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Apr 08 14:59:36 2014 +0200
    11.3 @@ -984,7 +984,7 @@
    11.4      (opt_modes -- Scan.option Parse.nat >> (fn (modes, limit) =>
    11.5        Toplevel.keep (fn state =>
    11.6         (if Isabelle_Process.is_active () then error "Illegal TTY command" else ();
    11.7 -        case limit of NONE => () | SOME n => Options.default_put_int @{option goals_limit} n;
    11.8 +        case limit of NONE => () | SOME n => Options.default_put_int @{system_option goals_limit} n;
    11.9          Toplevel.quiet := false;
   11.10          Print_Mode.with_modes modes (Toplevel.print_state true) state))));
   11.11  
    12.1 --- a/src/Pure/ML/ml_antiquotations.ML	Tue Apr 08 14:56:55 2014 +0200
    12.2 +++ b/src/Pure/ML/ml_antiquotations.ML	Tue Apr 08 14:59:36 2014 +0200
    12.3 @@ -8,17 +8,10 @@
    12.4  struct
    12.5  
    12.6  val _ = Theory.setup
    12.7 - (ML_Antiquotation.value @{binding option}
    12.8 + (ML_Antiquotation.value @{binding system_option}
    12.9      (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
   12.10 -      let
   12.11 -        val def_pos =
   12.12 -          Options.default_position name
   12.13 -            handle ERROR msg => error (msg ^ Position.here pos);
   12.14 -        val markup =
   12.15 -          Markup.properties (Position.def_properties_of def_pos)
   12.16 -            (Markup.entity Markup.system_optionN name);
   12.17 -        val _ = Context_Position.report ctxt pos markup;
   12.18 -      in ML_Syntax.print_string name end)) #>
   12.19 +      (Context_Position.report ctxt pos (Options.default_markup (name, pos));
   12.20 +        ML_Syntax.print_string name))) #>
   12.21  
   12.22    ML_Antiquotation.value @{binding theory}
   12.23      (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
    13.1 --- a/src/Pure/System/options.ML	Tue Apr 08 14:56:55 2014 +0200
    13.2 +++ b/src/Pure/System/options.ML	Tue Apr 08 14:59:36 2014 +0200
    13.3 @@ -13,7 +13,7 @@
    13.4    val unknownT: string
    13.5    type T
    13.6    val empty: T
    13.7 -  val position: T -> string -> Position.T
    13.8 +  val markup: T -> string * Position.T -> Markup.T
    13.9    val typ: T -> string -> string
   13.10    val bool: T -> string -> bool
   13.11    val int: T -> string -> int
   13.12 @@ -27,7 +27,7 @@
   13.13    val update: string -> string -> T -> T
   13.14    val decode: XML.body -> T
   13.15    val default: unit -> T
   13.16 -  val default_position: string -> Position.T
   13.17 +  val default_markup: string * Position.T -> Markup.T
   13.18    val default_typ: string -> string
   13.19    val default_bool: string -> bool
   13.20    val default_int: string -> int
   13.21 @@ -75,9 +75,19 @@
   13.22    end;
   13.23  
   13.24  
   13.25 -(* declaration *)
   13.26 +(* markup *)
   13.27  
   13.28 -fun position options name = #pos (check_name options name);
   13.29 +fun markup options (name, pos) =
   13.30 +  let
   13.31 +    val opt =
   13.32 +      check_name options name
   13.33 +        handle ERROR msg => error (msg ^ Position.here pos);
   13.34 +    val props = Position.def_properties_of (#pos opt);
   13.35 +  in Markup.properties props (Markup.entity Markup.system_optionN name) end;
   13.36 +
   13.37 +
   13.38 +(* typ *)
   13.39 +
   13.40  fun typ options name = #typ (check_name options name);
   13.41  
   13.42  
   13.43 @@ -173,7 +183,7 @@
   13.44      SOME options => options
   13.45    | NONE => err_no_default ());
   13.46  
   13.47 -fun default_position name = position (default ()) name;
   13.48 +fun default_markup arg = markup (default ()) arg;
   13.49  fun default_typ name = typ (default ()) name;
   13.50  fun default_bool name = bool (default ()) name;
   13.51  fun default_int name = int (default ()) name;
    14.1 --- a/src/Pure/Tools/find_theorems.ML	Tue Apr 08 14:56:55 2014 +0200
    14.2 +++ b/src/Pure/Tools/find_theorems.ML	Tue Apr 08 14:59:36 2014 +0200
    14.3 @@ -206,7 +206,7 @@
    14.4      val goal' = Thm.transfer thy' goal;
    14.5  
    14.6      fun limited_etac thm i =
    14.7 -      Seq.take (Options.default_int @{option find_theorems_tac_limit}) o etac thm i;
    14.8 +      Seq.take (Options.default_int @{system_option find_theorems_tac_limit}) o etac thm i;
    14.9      fun try_thm thm =
   14.10        if Thm.no_prems thm then rtac thm 1 goal'
   14.11        else
   14.12 @@ -405,7 +405,7 @@
   14.13            else raw_matches;
   14.14  
   14.15          val len = length matches;
   14.16 -        val lim = the_default (Options.default_int @{option find_theorems_limit}) opt_limit;
   14.17 +        val lim = the_default (Options.default_int @{system_option find_theorems_limit}) opt_limit;
   14.18        in (SOME len, drop (Int.max (len - lim, 0)) matches) end;
   14.19  
   14.20      val find =
    15.1 --- a/src/Pure/Tools/proof_general_pure.ML	Tue Apr 08 14:56:55 2014 +0200
    15.2 +++ b/src/Pure/Tools/proof_general_pure.ML	Tue Apr 08 14:59:36 2014 +0200
    15.3 @@ -17,49 +17,49 @@
    15.4  val _ =
    15.5    ProofGeneral.preference_option ProofGeneral.category_display
    15.6      NONE
    15.7 -    @{option show_types}
    15.8 +    @{system_option show_types}
    15.9      "show-types"
   15.10      "Include types in display of Isabelle terms";
   15.11  
   15.12  val _ =
   15.13    ProofGeneral.preference_option ProofGeneral.category_display
   15.14      NONE
   15.15 -    @{option show_sorts}
   15.16 +    @{system_option show_sorts}
   15.17      "show-sorts"
   15.18      "Include sorts in display of Isabelle types";
   15.19  
   15.20  val _ =
   15.21    ProofGeneral.preference_option ProofGeneral.category_display
   15.22      NONE
   15.23 -    @{option show_consts}
   15.24 +    @{system_option show_consts}
   15.25      "show-consts"
   15.26      "Show types of consts in Isabelle goal display";
   15.27  
   15.28  val _ =
   15.29    ProofGeneral.preference_option ProofGeneral.category_display
   15.30      NONE
   15.31 -    @{option names_long}
   15.32 +    @{system_option names_long}
   15.33      "long-names"
   15.34      "Show fully qualified names in Isabelle terms";
   15.35  
   15.36  val _ =
   15.37    ProofGeneral.preference_option ProofGeneral.category_display
   15.38      NONE
   15.39 -    @{option show_brackets}
   15.40 +    @{system_option show_brackets}
   15.41      "show-brackets"
   15.42      "Show full bracketing in Isabelle terms";
   15.43  
   15.44  val _ =
   15.45    ProofGeneral.preference_option ProofGeneral.category_display
   15.46      NONE
   15.47 -    @{option show_main_goal}
   15.48 +    @{system_option show_main_goal}
   15.49      "show-main-goal"
   15.50      "Show main goal in proof state display";
   15.51  
   15.52  val _ =
   15.53    ProofGeneral.preference_option ProofGeneral.category_display
   15.54      NONE
   15.55 -    @{option eta_contract}
   15.56 +    @{system_option eta_contract}
   15.57      "eta-contract"
   15.58      "Print terms eta-contracted";
   15.59  
   15.60 @@ -69,7 +69,7 @@
   15.61  val _ =
   15.62    ProofGeneral.preference_option ProofGeneral.category_advanced_display
   15.63      NONE
   15.64 -    @{option goals_limit}
   15.65 +    @{system_option goals_limit}
   15.66      "goals-limit"
   15.67      "Setting for maximum number of subgoals to be printed";
   15.68  
   15.69 @@ -85,7 +85,7 @@
   15.70  val _ =
   15.71    ProofGeneral.preference_option ProofGeneral.category_advanced_display
   15.72      NONE
   15.73 -    @{option show_question_marks}
   15.74 +    @{system_option show_question_marks}
   15.75      "show-question-marks"
   15.76      "Show leading question mark of variable name";
   15.77  
   15.78 @@ -123,7 +123,7 @@
   15.79  val _ =
   15.80    ProofGeneral.preference_option ProofGeneral.category_tracing
   15.81      NONE
   15.82 -    @{option ML_exception_trace}
   15.83 +    @{system_option ML_exception_trace}
   15.84      "debugging"
   15.85      "Whether to enable exception trace for toplevel command execution";
   15.86  
   15.87 @@ -140,14 +140,14 @@
   15.88  val _ =
   15.89    ProofGeneral.preference_option ProofGeneral.category_proof
   15.90      (SOME "true")
   15.91 -    @{option quick_and_dirty}
   15.92 +    @{system_option quick_and_dirty}
   15.93      "quick-and-dirty"
   15.94      "Take a few short cuts";
   15.95  
   15.96  val _ =
   15.97    ProofGeneral.preference_option ProofGeneral.category_proof
   15.98      NONE
   15.99 -    @{option skip_proofs}
  15.100 +    @{system_option skip_proofs}
  15.101      "skip-proofs"
  15.102      "Skip over proofs";
  15.103  
    16.1 --- a/src/Tools/quickcheck.ML	Tue Apr 08 14:56:55 2014 +0200
    16.2 +++ b/src/Tools/quickcheck.ML	Tue Apr 08 14:59:36 2014 +0200
    16.3 @@ -95,7 +95,7 @@
    16.4  val _ =
    16.5    ProofGeneral.preference_option ProofGeneral.category_tracing
    16.6      NONE
    16.7 -    @{option auto_quickcheck}
    16.8 +    @{system_option auto_quickcheck}
    16.9      "auto-quickcheck"
   16.10      "Run Quickcheck automatically";
   16.11  
   16.12 @@ -584,7 +584,7 @@
   16.13    end
   16.14    |> `(fn (outcome_code, _) => outcome_code = genuineN);
   16.15  
   16.16 -val _ = Try.tool_setup (quickcheckN, (20, @{option auto_quickcheck}, try_quickcheck));
   16.17 +val _ = Try.tool_setup (quickcheckN, (20, @{system_option auto_quickcheck}, try_quickcheck));
   16.18  
   16.19  end;
   16.20  
    17.1 --- a/src/Tools/solve_direct.ML	Tue Apr 08 14:56:55 2014 +0200
    17.2 +++ b/src/Tools/solve_direct.ML	Tue Apr 08 14:59:36 2014 +0200
    17.3 @@ -37,7 +37,7 @@
    17.4  val _ =
    17.5    ProofGeneral.preference_option ProofGeneral.category_tracing
    17.6      NONE
    17.7 -    @{option auto_solve_direct}
    17.8 +    @{system_option auto_solve_direct}
    17.9      "auto-solve-direct"
   17.10      ("Run " ^ quote solve_directN ^ " automatically");
   17.11  
   17.12 @@ -115,6 +115,6 @@
   17.13  
   17.14  fun try_solve_direct auto = do_solve_direct (if auto then Auto_Try else Try)
   17.15  
   17.16 -val _ = Try.tool_setup (solve_directN, (10, @{option auto_solve_direct}, try_solve_direct));
   17.17 +val _ = Try.tool_setup (solve_directN, (10, @{system_option auto_solve_direct}, try_solve_direct));
   17.18  
   17.19  end;
    18.1 --- a/src/Tools/try.ML	Tue Apr 08 14:56:55 2014 +0200
    18.2 +++ b/src/Tools/try.ML	Tue Apr 08 14:59:36 2014 +0200
    18.3 @@ -32,7 +32,7 @@
    18.4  val _ =
    18.5    ProofGeneral.preference_option ProofGeneral.category_tracing
    18.6      (SOME "4.0")
    18.7 -    @{option auto_time_limit}
    18.8 +    @{system_option auto_time_limit}
    18.9      "auto-try-time-limit"
   18.10      "Time limit for automatically tried tools (in seconds)"
   18.11  
   18.12 @@ -103,7 +103,7 @@
   18.13  
   18.14  val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state =>
   18.15    let
   18.16 -    val auto_time_limit = Options.default_real @{option auto_time_limit}
   18.17 +    val auto_time_limit = Options.default_real @{system_option auto_time_limit}
   18.18    in
   18.19      if interact andalso not (!Toplevel.quiet) andalso auto_time_limit > 0.0 then
   18.20        TimeLimit.timeLimit (seconds auto_time_limit) auto_try state
   18.21 @@ -120,7 +120,7 @@
   18.22      (fn {command_name, ...} =>
   18.23        if Keyword.is_theory_goal command_name andalso Options.default_bool auto then
   18.24          SOME
   18.25 -         {delay = SOME (seconds (Options.default_real @{option auto_time_start})),
   18.26 +         {delay = SOME (seconds (Options.default_real @{system_option auto_time_start})),
   18.27            pri = ~ weight,
   18.28            persistent = true,
   18.29            strict = true,
   18.30 @@ -128,7 +128,7 @@
   18.31              let
   18.32                val state = Toplevel.proof_of st
   18.33                  |> Proof.map_context (Context_Position.set_visible false)
   18.34 -              val auto_time_limit = Options.default_real @{option auto_time_limit}
   18.35 +              val auto_time_limit = Options.default_real @{system_option auto_time_limit}
   18.36              in
   18.37                if auto_time_limit > 0.0 then
   18.38                  (case TimeLimit.timeLimit (seconds auto_time_limit) (fn () => tool true state) () of