--- 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.
--- 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;