# HG changeset patch
# User wenzelm
# Date 1427222603 -3600
# Node ID af3e0919603f8a338057f45cfbe184a9f138e241
# Parent  0b21e85fd9bab62ddaa003657ac0535c023146a0
option to control old-style schematic mode;

diff -r 0b21e85fd9ba -r af3e0919603f src/Pure/Tools/rule_insts.ML
--- 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;