# HG changeset patch
# User wenzelm
# Date 1546527336 -3600
# Node ID cfac69e7b962393325bccf4946edca278b11c45f
# Parent  f77cc54f6d47b577e05e0915e7358e3fdfe49bf2
tuned signature;

diff -r f77cc54f6d47 -r cfac69e7b962 src/HOL/Tools/Argo/argo_tactic.ML
--- a/src/HOL/Tools/Argo/argo_tactic.ML	Thu Jan 03 14:12:44 2019 +0100
+++ b/src/HOL/Tools/Argo/argo_tactic.ML	Thu Jan 03 15:55:36 2019 +0100
@@ -79,7 +79,7 @@
 
 val timeout = Attrib.setup_config_real \<^binding>\<open>argo_timeout\<close> (K 10.0)
 
-fun time_of_timeout ctxt = Time.fromReal (Config.get ctxt timeout)
+val time_of_timeout = Time.fromReal o Config.apply timeout
 
 fun with_timeout ctxt f x = Timeout.apply (time_of_timeout ctxt) f x
 
diff -r f77cc54f6d47 -r cfac69e7b962 src/Pure/ML/ml_env.ML
--- a/src/Pure/ML/ml_env.ML	Thu Jan 03 14:12:44 2019 +0100
+++ b/src/Pure/ML/ml_env.ML	Thu Jan 03 15:55:36 2019 +0100
@@ -53,8 +53,8 @@
 val ML_read_global = Config.declare_bool ("ML_read_global", \<^here>) (K true);
 val ML_write_global = Config.declare_bool ("ML_write_global", \<^here>) (K true);
 
-fun read_global context = Config.get_generic context ML_read_global;
-fun write_global context = Config.get_generic context ML_write_global;
+val read_global = Config.apply_generic ML_read_global;
+val write_global = Config.apply_generic ML_write_global;
 
 
 (* name space tables *)
diff -r f77cc54f6d47 -r cfac69e7b962 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Thu Jan 03 14:12:44 2019 +0100
+++ b/src/Pure/Syntax/syntax.ML	Thu Jan 03 15:55:36 2019 +0100
@@ -323,7 +323,7 @@
 (* global pretty printing *)
 
 val pretty_global = Config.declare_bool ("Syntax.pretty_global", \<^here>) (K false);
-fun is_pretty_global ctxt = Config.get ctxt pretty_global;
+val is_pretty_global = Config.apply pretty_global;
 val set_pretty_global = Config.put pretty_global;
 val init_pretty_global = set_pretty_global true o Proof_Context.init_global;
 val init_pretty = Context.cases init_pretty_global I;
diff -r f77cc54f6d47 -r cfac69e7b962 src/Pure/config.ML
--- a/src/Pure/config.ML	Thu Jan 03 14:12:44 2019 +0100
+++ b/src/Pure/config.ML	Thu Jan 03 15:55:36 2019 +0100
@@ -12,14 +12,17 @@
   type 'a T
   val name_of: 'a T -> string
   val pos_of: 'a T -> Position.T
+  val apply: 'a T -> Proof.context -> 'a
   val get: Proof.context -> 'a T -> 'a
   val map: 'a T -> ('a -> 'a) -> Proof.context -> Proof.context
   val put: 'a T -> 'a -> Proof.context -> Proof.context
   val restore: 'a T -> Proof.context -> Proof.context -> Proof.context
+  val apply_global: 'a T -> theory -> 'a
   val get_global: theory -> 'a T -> 'a
   val map_global: 'a T -> ('a -> 'a) -> theory -> theory
   val put_global: 'a T -> 'a -> theory -> theory
   val restore_global: 'a T -> theory -> theory -> theory
+  val apply_generic: 'a T -> Context.generic -> 'a
   val get_generic: Context.generic -> 'a T -> 'a
   val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic
   val put_generic: 'a T -> 'a -> Context.generic -> Context.generic
@@ -92,20 +95,23 @@
 fun name_of (Config {name, ...}) = name;
 fun pos_of (Config {pos, ...}) = pos;
 
-fun get_generic context (Config {get_value, ...}) = get_value context;
+fun apply_generic (Config {get_value, ...}) = get_value;
+fun get_generic context config = apply_generic config context;
 fun map_generic (Config {map_value, ...}) f context = map_value f context;
 fun put_generic config value = map_generic config (K value);
-fun restore_generic config context = put_generic config (get_generic context config);
+fun restore_generic config = put_generic config o apply_generic config;
 
+fun apply_ctxt config = apply_generic config o Context.Proof;
 fun get_ctxt ctxt = get_generic (Context.Proof ctxt);
 fun map_ctxt config f = Context.proof_map (map_generic config f);
 fun put_ctxt config value = map_ctxt config (K value);
-fun restore_ctxt config ctxt = put_ctxt config (get_ctxt ctxt config);
+fun restore_ctxt config = put_ctxt config o apply_ctxt config;
 
+fun apply_global config = apply_generic config o Context.Theory;
 fun get_global thy = get_generic (Context.Theory thy);
 fun map_global config f = Context.theory_map (map_generic config f);
 fun put_global config value = map_global config (K value);
-fun restore_global config thy = put_global config (get_global thy config);
+fun restore_global config = put_global config o apply_global config;
 
 
 (* coerce type *)
@@ -174,6 +180,7 @@
 val declare_option_string = string o declare_option;
 
 (*final declarations of this structure!*)
+val apply = apply_ctxt;
 val get = get_ctxt;
 val map = map_ctxt;
 val put = put_ctxt;
diff -r f77cc54f6d47 -r cfac69e7b962 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Thu Jan 03 14:12:44 2019 +0100
+++ b/src/Pure/variable.ML	Thu Jan 03 15:55:36 2019 +0100
@@ -335,16 +335,16 @@
 (* inner body mode *)
 
 val inner_body = Config.declare_bool ("inner_body", \<^here>) (K false);
-fun is_body ctxt = Config.get ctxt inner_body;
+val is_body = Config.apply inner_body;
 val set_body = Config.put inner_body;
-fun restore_body ctxt = set_body (is_body ctxt);
+val restore_body = set_body o is_body;
 
 
 (* proper mode *)
 
 val proper_fixes = Config.declare_bool ("proper_fixes", \<^here>) (K true);
 val improper_fixes = Config.put proper_fixes false;
-fun restore_proper_fixes ctxt = Config.put proper_fixes (Config.get ctxt proper_fixes);
+val restore_proper_fixes = Config.put proper_fixes o Config.apply proper_fixes;
 
 fun is_improper ctxt x =
   (case Name_Space.lookup (fixes_of ctxt) x of
@@ -641,9 +641,9 @@
 (* focus on outermost parameters: \<And>x y z. B *)
 
 val bound_focus = Config.declare_bool ("bound_focus", \<^here>) (K false);
-fun is_bound_focus ctxt = Config.get ctxt bound_focus;
+val is_bound_focus = Config.apply bound_focus;
 val set_bound_focus = Config.put bound_focus;
-fun restore_bound_focus ctxt = set_bound_focus (is_bound_focus ctxt);
+val restore_bound_focus = set_bound_focus o is_bound_focus;
 
 fun focus_params bindings t ctxt =
   let