discontinued legacy;
authorwenzelm
Mon Jun 01 15:06:09 2015 +0200 (2015-06-01)
changeset 60331f215fd466e30
parent 60330 a40b43121c5f
child 60332 7676bcaa1f95
discontinued legacy;
NEWS
src/Pure/Tools/rule_insts.ML
     1.1 --- a/NEWS	Mon Jun 01 13:52:35 2015 +0200
     1.2 +++ b/NEWS	Mon Jun 01 15:06:09 2015 +0200
     1.3 @@ -3,9 +3,16 @@
     1.4  
     1.5  (Note: Isabelle/jEdit shows a tree-view of this file in Sidekick.)
     1.6  
     1.7 +
     1.8  New in this Isabelle version
     1.9  ----------------------------
    1.10  
    1.11 +*** Pure ***
    1.12 +
    1.13 +* Configuration option rule_insts_schematic has been discontinued
    1.14 +(intermediate legacy feature in Isabelle2015).  INCOMPATIBILITY.
    1.15 +
    1.16 +
    1.17  *** HOL ***
    1.18  
    1.19  * Discontinued simp_legacy_precond. Potential INCOMPATIBILITY.
     2.1 --- a/src/Pure/Tools/rule_insts.ML	Mon Jun 01 13:52:35 2015 +0200
     2.2 +++ b/src/Pure/Tools/rule_insts.ML	Mon Jun 01 15:06:09 2015 +0200
     2.3 @@ -14,7 +14,6 @@
     2.4    val read_instantiate: Proof.context ->
     2.5      ((indexname * Position.T) * string) list -> string list -> thm -> thm
     2.6    val read_term: string -> Proof.context -> term * Proof.context
     2.7 -  val schematic: bool Config.T
     2.8    val goal_context: term -> Proof.context -> (string * typ) list * Proof.context
     2.9    val res_inst_tac: Proof.context ->
    2.10      ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list ->
    2.11 @@ -214,17 +213,13 @@
    2.12  
    2.13  (* goal context *)
    2.14  
    2.15 -(*legacy*)
    2.16 -val schematic = Attrib.setup_config_bool @{binding rule_insts_schematic} (K false);
    2.17 -
    2.18  fun goal_context goal ctxt =
    2.19    let
    2.20      val ((_, params), ctxt') = ctxt
    2.21        |> Variable.declare_constraints goal
    2.22        |> Variable.improper_fixes
    2.23        |> Variable.focus_params goal
    2.24 -      ||> Variable.restore_proper_fixes ctxt
    2.25 -      ||> Config.get ctxt schematic ? Proof_Context.set_mode Proof_Context.mode_schematic;
    2.26 +      ||> Variable.restore_proper_fixes ctxt;
    2.27    in (params, ctxt') end;
    2.28  
    2.29