# HG changeset patch
# User wenzelm
# Date 1662668382 -7200
# Node ID 282f5e980a67a0d3eda7965916167b01729d4e4f
# Parent  922e3f9251acebfabfd590a43158a3746fd2c106
discontinue fragile operations;

diff -r 922e3f9251ac -r 282f5e980a67 src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Thu Sep 08 22:06:06 2022 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Thu Sep 08 22:19:42 2022 +0200
@@ -285,7 +285,7 @@
        #> Sledgehammer_MePo.mepo_suggested_facts ctxt params max_suggs NONE hyp_ts concl_t)
 
 fun generate_mash_suggestions algorithm ctxt =
-  (Options.put_default \<^system_option>\<open>MaSh\<close> algorithm;
+  (Options.put_default \<^system_option>\<open>MaSh\<close> algorithm;  (* FIXME fragile *)
    Sledgehammer_MaSh.mash_unlearn ctxt;
    generate_mepo_or_mash_suggestions
      (fn ctxt => fn thy_name => fn params as {provers = prover :: _, ...} =>
diff -r 922e3f9251ac -r 282f5e980a67 src/Pure/System/options.ML
--- a/src/Pure/System/options.ML	Thu Sep 08 22:06:06 2022 +0200
+++ b/src/Pure/System/options.ML	Thu Sep 08 22:19:42 2022 +0200
@@ -35,10 +35,6 @@
   val default_real: string -> real
   val default_seconds: string -> Time.time
   val default_string: string -> string
-  val default_put_bool: string -> bool -> unit
-  val default_put_int: string -> int -> unit
-  val default_put_real: string -> real -> unit
-  val default_put_string: string -> string -> unit
   val get_default: string -> string
   val put_default: string -> string -> unit
   val set_default: T -> unit
@@ -195,11 +191,6 @@
 fun default_seconds name = seconds (default ()) name;
 fun default_string name = string (default ()) name;
 
-val default_put_bool = change_default put_bool;
-val default_put_int = change_default put_int;
-val default_put_real = change_default put_real;
-val default_put_string = change_default put_string;
-
 fun get_default name =
   let val options = default () in get (typ options name) SOME options name end;
 val put_default = change_default update;