# HG changeset patch
# User wenzelm
# Date 1433163969 -7200
# Node ID f215fd466e30be4d26f60e96f56b8566471bd1bb
# Parent  a40b43121c5f17b3029aa1248384908bb5dfc9ff
discontinued legacy;

diff -r a40b43121c5f -r f215fd466e30 NEWS
--- a/NEWS	Mon Jun 01 13:52:35 2015 +0200
+++ b/NEWS	Mon Jun 01 15:06:09 2015 +0200
@@ -3,9 +3,16 @@
 
 (Note: Isabelle/jEdit shows a tree-view of this file in Sidekick.)
 
+
 New in this Isabelle version
 ----------------------------
 
+*** Pure ***
+
+* Configuration option rule_insts_schematic has been discontinued
+(intermediate legacy feature in Isabelle2015).  INCOMPATIBILITY.
+
+
 *** HOL ***
 
 * Discontinued simp_legacy_precond. Potential INCOMPATIBILITY.
diff -r a40b43121c5f -r f215fd466e30 src/Pure/Tools/rule_insts.ML
--- a/src/Pure/Tools/rule_insts.ML	Mon Jun 01 13:52:35 2015 +0200
+++ b/src/Pure/Tools/rule_insts.ML	Mon Jun 01 15:06:09 2015 +0200
@@ -14,7 +14,6 @@
   val read_instantiate: Proof.context ->
     ((indexname * Position.T) * string) list -> string list -> thm -> thm
   val read_term: string -> Proof.context -> term * Proof.context
-  val schematic: bool Config.T
   val goal_context: term -> Proof.context -> (string * typ) list * Proof.context
   val res_inst_tac: Proof.context ->
     ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list ->
@@ -214,17 +213,13 @@
 
 (* goal context *)
 
-(*legacy*)
-val schematic = Attrib.setup_config_bool @{binding rule_insts_schematic} (K false);
-
 fun goal_context goal ctxt =
   let
     val ((_, params), ctxt') = ctxt
       |> Variable.declare_constraints goal
       |> Variable.improper_fixes
       |> Variable.focus_params goal
-      ||> Variable.restore_proper_fixes ctxt
-      ||> Config.get ctxt schematic ? Proof_Context.set_mode Proof_Context.mode_schematic;
+      ||> Variable.restore_proper_fixes ctxt;
   in (params, ctxt') end;