# HG changeset patch
# User wenzelm
# Date 1427638955 -7200
# Node ID 97872c658a44198995b0ef360261c05bbe0a4298
# Parent  fc3d7eaa486e844a9b7e7cab8c6ba02fe7475fe7
rule_insts_schematic is considered legacy and false by default;

diff -r fc3d7eaa486e -r 97872c658a44 NEWS
--- a/NEWS	Sun Mar 29 16:01:12 2015 +0200
+++ b/NEWS	Sun Mar 29 16:22:35 2015 +0200
@@ -61,15 +61,19 @@
 
 *** Pure ***
 
-* Proof methods with explicit instantiation ("rule_tac", "subgoal_tac"
-etc.) allow an optional context of local variables ('for' declaration):
-these variables become schematic in the instantiated theorem. This
-behaviour is analogous to 'for' in attributes "where" and "of".
-
 * Explicit instantiation via attributes "where", "of", and proof methods
 "rule_tac" with derivatives like "subgoal_tac" etc. admit dummy patterns
 ("_") that stand for anonymous local variables.
 
+* Proof methods with explicit instantiation ("rule_tac", "subgoal_tac"
+etc.) allow an optional context of local variables ('for' declaration):
+these variables become schematic in the instantiated theorem; this
+behaviour is analogous to 'for' in attributes "where" and "of".
+Configuration option rule_insts_schematic (default false) controls use
+of schematic variables outside the context. Minor INCOMPATIBILITY,
+declare rule_insts_schematic = true temporarily and update to use local
+variable declarations or dummy patterns instead.
+
 * Configuration option "rule_insts_schematic" determines whether proof
 methods like "rule_tac" may refer to undeclared schematic variables
 implicitly, instead of using proper 'for' declarations.  This historic
diff -r fc3d7eaa486e -r 97872c658a44 src/Pure/Tools/rule_insts.ML
--- a/src/Pure/Tools/rule_insts.ML	Sun Mar 29 16:01:12 2015 +0200
+++ b/src/Pure/Tools/rule_insts.ML	Sun Mar 29 16:22:35 2015 +0200
@@ -209,7 +209,8 @@
 
 (* goal context *)
 
-val schematic = Attrib.setup_config_bool @{binding rule_insts_schematic} (K true);
+(*legacy*)
+val schematic = Attrib.setup_config_bool @{binding rule_insts_schematic} (K false);
 
 fun goal_context goal ctxt =
   let
@@ -232,7 +233,7 @@
     val paramTs = map #2 params;
 
 
-    (* local fixes and instantiation *)
+    (* instantiation context *)
 
     val ((inst_tvars, inst_vars), inst_ctxt) = goal_ctxt
       |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2