diff -r af3e0919603f -r ca948c89828e src/Pure/Tools/rule_insts.ML
--- a/src/Pure/Tools/rule_insts.ML	Tue Mar 24 19:43:23 2015 +0100
+++ b/src/Pure/Tools/rule_insts.ML	Tue Mar 24 20:07:27 2015 +0100
@@ -13,7 +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 schematic: bool Config.T
   val res_inst_tac: Proof.context ->
     ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> thm ->
     int -> tactic
@@ -199,7 +199,7 @@
 
 (** tactics **)
 
-val insts_schematic = Attrib.setup_config_bool @{binding insts_schematic} (K true);
+val schematic = Attrib.setup_config_bool @{binding rule_insts_schematic} (K true);
 
 (* resolution after lifting and instantiation; may refer to parameters of the subgoal *)
 
@@ -219,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
-      ||> Config.get ctxt insts_schematic ? Proof_Context.set_mode Proof_Context.mode_schematic;
+      ||> Config.get ctxt schematic ? Proof_Context.set_mode Proof_Context.mode_schematic;
     val paramTs = map #2 params;