--- a/src/Pure/Tools/rule_insts.ML Tue Mar 24 18:36:29 2015 +0100
+++ b/src/Pure/Tools/rule_insts.ML Tue Mar 24 19:43:23 2015 +0100
@@ -13,6 +13,7 @@
(binding * string option * mixfix) list -> thm -> thm
val read_instantiate: Proof.context ->
((indexname * Position.T) * string) list -> string list -> thm -> thm
+ val insts_schematic: bool Config.T
val res_inst_tac: Proof.context ->
((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> thm ->
int -> tactic
@@ -198,6 +199,8 @@
(** tactics **)
+val insts_schematic = Attrib.setup_config_bool @{binding insts_schematic} (K true);
+
(* resolution after lifting and instantiation; may refer to parameters of the subgoal *)
fun bires_inst_tac bires_flag ctxt mixed_insts fixes thm i st = CSUBGOAL (fn (cgoal, _) =>
@@ -216,7 +219,7 @@
|> Variable.improper_fixes
|> Proof_Context.add_fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params)
||> Variable.restore_proper_fixes ctxt
- ||> Proof_Context.set_mode Proof_Context.mode_schematic;
+ ||> Config.get ctxt insts_schematic ? Proof_Context.set_mode Proof_Context.mode_schematic;
val paramTs = map #2 params;