# 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>\MaSh\ algorithm; + (Options.put_default \<^system_option>\MaSh\ 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;